diff options
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 29 |
1 files changed, 19 insertions, 10 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 09c81c7d7..b807c2d7f 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -15,9 +15,9 @@ open Environ open Evd (* An inductive type with its parameters *) -type inductive_family = inductive * constr list -val make_ind_family : 'a * 'b -> 'a * 'b -val dest_ind_family : 'a * 'b -> 'a * 'b +type inductive_family +val make_ind_family : inductive * constr list -> inductive_family +val dest_ind_family : inductive_family -> inductive * constr list val liftn_inductive_family : int -> int -> inductive_family -> inductive_family val lift_inductive_family : int -> inductive_family -> inductive_family val substnl_ind_family : @@ -49,23 +49,31 @@ val lift_constructor : int -> constructor_summary -> constructor_summary val get_constructor : inductive * mutual_inductive_body * one_inductive_body * constr list -> int -> constructor_summary -val get_constructors : - env -> inductive * constr list -> constructor_summary array -val get_arity : env -> inductive * constr list -> Sign.arity +val get_arity : env -> inductive_family -> Sign.arity +val get_constructors : env -> inductive_family -> constructor_summary array val build_dependent_constructor : constructor_summary -> constr -val build_dependent_inductive : env -> inductive * constr list -> constr +val build_dependent_inductive : env -> inductive_family -> constr val make_arity_signature : - env -> bool -> inductive * constr list -> Sign.rel_context -val make_arity : env -> bool -> inductive * constr list -> sorts -> types + env -> bool -> inductive_family -> Sign.rel_context +val make_arity : env -> bool -> inductive_family -> sorts -> types val build_branch_type : env -> bool -> constr -> constructor_summary -> types -exception Induc +(* Raise Not_found if not given an valid inductive type *) val extract_mrectype : constr -> inductive * constr list val find_mrectype : env -> evar_map -> constr -> inductive * constr list val find_rectype : env -> evar_map -> constr -> inductive_type 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 : + env -> inductive_family -> bool -> sorts -> types + val type_case_branches_with_names : env -> inductive * constr list -> unsafe_judgment -> constr -> types array * types @@ -73,4 +81,5 @@ val make_case_info : env -> inductive -> case_style option -> pattern_source array -> case_info val make_default_case_info : env -> inductive -> case_info +(********************) val control_only_guard : env -> types -> unit |