diff options
| author | Pierre-Marie Pédrot | 2019-03-14 19:00:34 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-10 15:03:19 +0200 |
| commit | 2a79abc613bdf19b53685a40c993f964455904fe (patch) | |
| tree | c0fd8ab20f683c3141934d060852dcda0d569f00 /pretyping/coercionops.mli | |
| parent | aab47903fb2d3e0085b03d5ade94f4ae644cd76c (diff) | |
No more local reduction functions in Reductionops.
This is extracted from #9710, where we need the environment anyway to compute
iota rules on inductive types with let-bindings. The commit is self-contained,
so I think it could go directly in to save me a few rebases.
Furthermore, this is also related to #11707. Assuming we split cbn from the
other reduction machine, this allows to merge the "local" machine with
the general one, since after this PR they will have the same type. One less
reduction machine should make people happy.
Diffstat (limited to 'pretyping/coercionops.mli')
| -rw-r--r-- | pretyping/coercionops.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli index 247ef4df75..31600dd17f 100644 --- a/pretyping/coercionops.mli +++ b/pretyping/coercionops.mli @@ -26,7 +26,7 @@ type cl_typ = (** Equality over [cl_typ] *) val cl_typ_eq : cl_typ -> cl_typ -> bool -val subst_cl_typ : substitution -> cl_typ -> cl_typ +val subst_cl_typ : env -> substitution -> cl_typ -> cl_typ (** Comparison of [cl_typ] *) val cl_typ_ord : cl_typ -> cl_typ -> int @@ -64,7 +64,7 @@ val class_info_from_index : cl_index -> cl_typ * cl_info_typ (** [find_class_type env sigma c] returns the head reference of [c], its universe instance and its arguments *) -val find_class_type : evar_map -> types -> cl_typ * EInstance.t * constr list +val find_class_type : env -> evar_map -> types -> cl_typ * EInstance.t * constr list (** raises [Not_found] if not convertible to a class *) val class_of : env -> evar_map -> types -> types * cl_index |