summaryrefslogtreecommitdiff
path: root/toplevel/auto_ind_decl.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /toplevel/auto_ind_decl.mli
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'toplevel/auto_ind_decl.mli')
-rw-r--r--toplevel/auto_ind_decl.mli32
1 files changed, 23 insertions, 9 deletions
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli
index b8fa1710..855f023f 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.mli
@@ -11,17 +11,31 @@ open Names
open Libnames
open Mod_subst
open Sign
+open Proof_type
+open Ind_tables
+(* Build boolean equality of a block of mutual inductive types *)
-val subst_in_constr : (object_name*substitution*(inductive*constr))
- -> (inductive*constr)
+exception EqNotFound of inductive * inductive
+exception EqUnknown of string
+exception UndefinedCst of string
+exception InductiveWithProduct
+exception InductiveWithSort
+exception ParameterWithoutEquality of constant
+exception NonSingletonProp of inductive
-val compute_bl_goal : inductive -> rel_context -> int -> types
-val compute_bl_tact : inductive -> rel_context -> int -> unit
-val compute_lb_goal : inductive -> rel_context -> int -> types
-val compute_lb_tact : inductive -> rel_context -> int -> unit
-val compute_dec_goal : inductive -> rel_context -> int -> types
-val compute_dec_tact : inductive -> rel_context -> int -> unit
+val beq_scheme_kind : mutual scheme_kind
+val build_beq_scheme : mutual_inductive -> constr array
+(* Build equivalence between boolean equality and Leibniz equality *)
-val make_eq_scheme :mutual_inductive -> types array
+val lb_scheme_kind : mutual scheme_kind
+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 *)
+
+val eq_dec_scheme_kind : mutual scheme_kind
+val make_eq_decidability : mutual_inductive -> constr array