package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b
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