package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.18.0.tar.gz
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50
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