diff options
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*) |