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