package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c
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