diff options
Diffstat (limited to 'toplevel/auto_ind_decl.mli')
| -rw-r--r-- | toplevel/auto_ind_decl.mli | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli index 1cb8b767..5dbd5379 100644 --- a/toplevel/auto_ind_decl.mli +++ b/toplevel/auto_ind_decl.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,10 +8,6 @@ open Term open Names -open Libnames -open Mod_subst -open Sign -open Proof_type open Ind_tables (** This file is about the automatic generation of schemes about @@ -30,17 +26,16 @@ exception ParameterWithoutEquality of constant exception NonSingletonProp of inductive val beq_scheme_kind : mutual scheme_kind -val build_beq_scheme : mutual_inductive -> constr array +val build_beq_scheme : mutual_scheme_object_function (** {6 Build equivalence between boolean equality and Leibniz equality } *) val lb_scheme_kind : mutual scheme_kind -val make_lb_scheme : mutual_inductive -> constr array - +val make_lb_scheme : mutual_scheme_object_function val bl_scheme_kind : mutual scheme_kind -val make_bl_scheme : mutual_inductive -> constr array +val make_bl_scheme : mutual_scheme_object_function (** {6 Build decidability of equality } *) val eq_dec_scheme_kind : mutual scheme_kind -val make_eq_decidability : mutual_inductive -> constr array +val make_eq_decidability : mutual_scheme_object_function |