diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /pretyping/inductiveops.mli | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'pretyping/inductiveops.mli')
-rw-r--r-- | pretyping/inductiveops.mli | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 1cf940cb..a9a51d9a 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 11436 2008-10-07 13:56:55Z barras $ i*) +(*i $Id$ i*) open Names open Term @@ -58,7 +58,9 @@ val mis_nf_constructor_type : val mis_constr_nargs : inductive -> int array val mis_constr_nargs_env : env -> inductive -> int array -(* Return number of expected parameters and of expected real arguments *) +val nconstructors : inductive -> int + +(* Return the lengths of parameters signature and real arguments signature *) val inductive_nargs : env -> inductive -> int * int val mis_constructor_nargs_env : env -> constructor -> int @@ -75,7 +77,7 @@ type constructor_summary = { cs_cstr : constructor; cs_params : constr list; cs_nargs : int; - cs_args : Sign.rel_context; + cs_args : rel_context; cs_concl_realargs : constr array; } val lift_constructor : int -> constructor_summary -> constructor_summary @@ -86,7 +88,7 @@ val get_arity : env -> inductive_family -> rel_context * sorts_family val get_constructors : env -> inductive_family -> constructor_summary array val build_dependent_constructor : constructor_summary -> constr val build_dependent_inductive : env -> inductive_family -> constr -val make_arity_signature : env -> bool -> inductive_family -> Sign.rel_context +val make_arity_signature : env -> bool -> inductive_family -> rel_context val make_arity : env -> bool -> inductive_family -> sorts -> types val build_branch_type : env -> bool -> constr -> constructor_summary -> types @@ -104,11 +106,11 @@ val arity_of_case_predicate : env -> inductive_family -> bool -> sorts -> types val type_case_branches_with_names : - env -> inductive * constr list -> unsafe_judgment -> constr -> + env -> inductive * constr list -> constr -> constr -> types array * types val make_case_info : env -> inductive -> case_style -> case_info -(*i Compatibility +(*i Compatibility val make_default_case_info : env -> case_style -> inductive -> case_info i*) |