package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.16.1.tar.gz
sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b
doc/src/funind_plugin/funind_plugin.ml.html
Source file funind_plugin.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31(* generated by dune *) (** @canonical Funind_plugin.Functional_principles_proofs *) module Functional_principles_proofs = Funind_plugin__Functional_principles_proofs (** @canonical Funind_plugin.Functional_principles_types *) module Functional_principles_types = Funind_plugin__Functional_principles_types (** @canonical Funind_plugin.G_indfun *) module G_indfun = Funind_plugin__G_indfun (** @canonical Funind_plugin.Gen_principle *) module Gen_principle = Funind_plugin__Gen_principle (** @canonical Funind_plugin.Glob_term_to_relation *) module Glob_term_to_relation = Funind_plugin__Glob_term_to_relation (** @canonical Funind_plugin.Glob_termops *) module Glob_termops = Funind_plugin__Glob_termops (** @canonical Funind_plugin.Indfun *) module Indfun = Funind_plugin__Indfun (** @canonical Funind_plugin.Indfun_common *) module Indfun_common = Funind_plugin__Indfun_common (** @canonical Funind_plugin.Invfun *) module Invfun = Funind_plugin__Invfun (** @canonical Funind_plugin.Recdef *) module Recdef = Funind_plugin__Recdef