diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
| commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
| tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /pretyping/inductiveops.mli | |
| parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) | |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 23 |
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 |