diff options
Diffstat (limited to 'toplevel/auto_ind_decl.mli')
| -rw-r--r-- | toplevel/auto_ind_decl.mli | 25 |
1 files changed, 15 insertions, 10 deletions
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli index 855f023f5..901ddb721 100644 --- a/toplevel/auto_ind_decl.mli +++ b/toplevel/auto_ind_decl.mli @@ -1,10 +1,10 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) open Term open Names @@ -14,7 +14,12 @@ open Sign open Proof_type open Ind_tables -(* Build boolean equality of a block of mutual inductive types *) +(** This file is about the automatic generation of schemes about + decidable equality, + @author Vincent Siles + Oct 2007 *) + +(** {6 Build boolean equality of a block of mutual inductive types } *) exception EqNotFound of inductive * inductive exception EqUnknown of string @@ -27,7 +32,7 @@ exception NonSingletonProp of inductive val beq_scheme_kind : mutual scheme_kind val build_beq_scheme : mutual_inductive -> constr array -(* Build equivalence between boolean equality and Leibniz equality *) +(** {6 Build equivalence between boolean equality and Leibniz equality } *) val lb_scheme_kind : mutual scheme_kind val make_lb_scheme : mutual_inductive -> constr array @@ -35,7 +40,7 @@ val make_lb_scheme : mutual_inductive -> constr array val bl_scheme_kind : mutual scheme_kind val make_bl_scheme : mutual_inductive -> constr array -(* Build decidability of equality *) +(** {6 Build decidability of equality } *) val eq_dec_scheme_kind : mutual scheme_kind val make_eq_decidability : mutual_inductive -> constr array |