diff options
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 7bd616591..bdb6f996b 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -37,15 +37,15 @@ val substnl_ind_family : constr list -> int -> inductive_family -> inductive_family (** An inductive type with its parameters and real arguments *) -type inductive_type = IndType of inductive_family * constr list -val make_ind_type : inductive_family * constr list -> inductive_type -val dest_ind_type : inductive_type -> inductive_family * constr list -val map_inductive_type : (constr -> constr) -> inductive_type -> inductive_type +type inductive_type = IndType of inductive_family * EConstr.constr list +val make_ind_type : inductive_family * EConstr.constr list -> inductive_type +val dest_ind_type : inductive_type -> inductive_family * EConstr.constr list +val map_inductive_type : (EConstr.constr -> EConstr.constr) -> inductive_type -> inductive_type val liftn_inductive_type : int -> int -> inductive_type -> inductive_type val lift_inductive_type : int -> inductive_type -> inductive_type -val substnl_ind_type : constr list -> int -> inductive_type -> inductive_type +val substnl_ind_type : EConstr.constr list -> int -> inductive_type -> inductive_type -val mkAppliedInd : inductive_type -> constr +val mkAppliedInd : inductive_type -> EConstr.constr val mis_is_recursive_subset : int list -> wf_paths -> bool val mis_is_recursive : inductive * mutual_inductive_body * one_inductive_body -> bool @@ -130,7 +130,7 @@ val has_dependent_elim : mutual_inductive_body -> bool val projection_nparams : projection -> int val projection_nparams_env : env -> projection -> int val type_of_projection_knowing_arg : env -> evar_map -> Projection.t -> - constr -> types -> types + EConstr.t -> EConstr.types -> types (** Extract information from an inductive family *) @@ -156,17 +156,17 @@ val get_arity : env -> inductive_family -> Context.Rel.t * sorts_family val build_dependent_constructor : constructor_summary -> constr val build_dependent_inductive : env -> inductive_family -> constr -val make_arity_signature : env -> bool -> inductive_family -> Context.Rel.t -val make_arity : env -> bool -> inductive_family -> sorts -> types -val build_branch_type : env -> bool -> constr -> constructor_summary -> types +val make_arity_signature : env -> evar_map -> bool -> inductive_family -> EConstr.rel_context +val make_arity : env -> evar_map -> bool -> inductive_family -> sorts -> EConstr.types +val build_branch_type : env -> evar_map -> bool -> constr -> constructor_summary -> types (** Raise [Not_found] if not given a valid inductive type *) -val extract_mrectype : constr -> pinductive * constr list -val find_mrectype : env -> evar_map -> types -> pinductive * constr list -val find_mrectype_vect : env -> evar_map -> types -> pinductive * constr array -val find_rectype : env -> evar_map -> types -> inductive_type -val find_inductive : env -> evar_map -> types -> pinductive * constr list -val find_coinductive : env -> evar_map -> types -> pinductive * constr list +val extract_mrectype : evar_map -> EConstr.t -> (inductive * EConstr.EInstance.t) * EConstr.constr list +val find_mrectype : env -> evar_map -> EConstr.types -> (inductive * EConstr.EInstance.t) * EConstr.constr list +val find_mrectype_vect : env -> evar_map -> EConstr.types -> (inductive * EConstr.EInstance.t) * EConstr.constr array +val find_rectype : env -> evar_map -> EConstr.types -> inductive_type +val find_inductive : env -> evar_map -> EConstr.types -> (inductive * EConstr.EInstance.t) * constr list +val find_coinductive : env -> evar_map -> EConstr.types -> (inductive * EConstr.EInstance.t) * constr list (********************) @@ -175,7 +175,7 @@ val arity_of_case_predicate : env -> inductive_family -> bool -> sorts -> types val type_case_branches_with_names : - env -> pinductive * constr list -> constr -> constr -> types array * types + env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> types array * types (** Annotation for cases *) val make_case_info : env -> inductive -> case_style -> case_info @@ -185,8 +185,8 @@ val make_case_info : env -> inductive -> case_style -> case_info Fail with an error if the elimination is dependent while the inductive type does not allow dependent elimination. *) val make_case_or_project : - env -> inductive_family -> case_info -> - (* pred *) constr -> (* term *) constr -> (* branches *) constr array -> constr + env -> evar_map -> inductive_family -> case_info -> + (* pred *) EConstr.constr -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr (*i Compatibility val make_default_case_info : env -> case_style -> inductive -> case_info @@ -195,7 +195,7 @@ i*) (********************) val type_of_inductive_knowing_conclusion : - env -> evar_map -> Inductive.mind_specif puniverses -> types -> evar_map * types + env -> evar_map -> Inductive.mind_specif puniverses -> EConstr.types -> evar_map * EConstr.types (********************) val control_only_guard : env -> types -> unit |