diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-01 20:53:32 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:21:51 +0100 |
| commit | 8f6aab1f4d6d60842422abc5217daac806eb0897 (patch) | |
| tree | c36f2f963064f51fe1652714f4d91677d555727b /pretyping/inductiveops.mli | |
| parent | 5143129baac805d3a49ac3ee9f3344c7a447634f (diff) | |
Reductionops API using EConstr.
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 7bd616591..1cfdef6e5 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -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 *) @@ -161,12 +161,12 @@ val make_arity : env -> bool -> inductive_family -> sorts -> types val build_branch_type : env -> 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 -> pinductive * constr list +val find_mrectype : env -> evar_map -> EConstr.types -> pinductive * constr list +val find_mrectype_vect : env -> evar_map -> EConstr.types -> pinductive * constr array +val find_rectype : env -> evar_map -> EConstr.types -> inductive_type +val find_inductive : env -> evar_map -> EConstr.types -> pinductive * constr list +val find_coinductive : env -> evar_map -> EConstr.types -> pinductive * 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 * constr list -> constr -> constr -> types array * types (** Annotation for cases *) val make_case_info : env -> inductive -> case_style -> 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 * types (********************) val control_only_guard : env -> types -> unit |