summaryrefslogtreecommitdiff
path: root/pretyping/inductiveops.mli
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /pretyping/inductiveops.mli
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'pretyping/inductiveops.mli')
-rw-r--r--pretyping/inductiveops.mli23
1 files changed, 19 insertions, 4 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 8cfa9b3c..2993eed3 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: inductiveops.mli,v 1.10.2.3 2005/01/21 17:19:37 herbelin Exp $ i*)
+(*i $Id: inductiveops.mli 7955 2006-01-30 22:56:15Z herbelin $ i*)
open Names
open Term
@@ -14,6 +14,17 @@ open Declarations
open Environ
open Evd
+(* The following three functions are similar to the ones defined in
+ Inductive, but they expect an env *)
+
+val type_of_inductive : env -> inductive -> types
+
+(* Return type as quoted by the user *)
+val type_of_constructor : env -> constructor -> types
+
+(* Return constructor types in normal form *)
+val arities_of_constructors : env -> inductive -> types array
+
(* An inductive type with its parameters *)
type inductive_family
val make_ind_family : inductive * constr list -> inductive_family
@@ -46,6 +57,11 @@ val mis_constr_nargs_env : env -> inductive -> int array
val mis_constructor_nargs_env : env -> constructor -> int
+val constructor_nrealargs : env -> constructor -> int
+val constructor_nrealhyps : env -> constructor -> int
+
+val inductive_nargs : env -> inductive -> int
+
type constructor_summary = {
cs_cstr : constructor;
cs_params : constr list;
@@ -74,9 +90,6 @@ val find_inductive : env -> evar_map -> constr -> inductive * constr list
val find_coinductive : env -> evar_map -> constr -> inductive * constr list
(********************)
-(* Determines if a case predicate type corresponds to dependent elimination *)
-val is_dependent_elimination :
- env -> types -> inductive_family -> bool
(* Builds the case predicate arity (dependent or not) *)
val arity_of_case_predicate :
@@ -91,3 +104,5 @@ val make_default_case_info : env -> case_style -> inductive -> case_info
(********************)
val control_only_guard : env -> types -> unit
+
+val subst_inductive : Mod_subst.substitution -> inductive -> inductive