diff options
| author | Pierre-Marie Pédrot | 2019-12-24 14:19:56 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-26 12:42:31 +0100 |
| commit | 9d0e4b2ab78b89e39c63e8010ffd03745b309b5a (patch) | |
| tree | 98bbde69fba3fb77d2d7705c55cfbed781570368 /pretyping/evarsolve.mli | |
| parent | feea1d0377e2fb083efe74cd241e7867d008d5be (diff) | |
Remove uses of Global in Evd API.
Namely, Evd.evar_env and Evd.evar_filtered_env now take an additional
environment instead of querying the imperative global one. We percolate
this change as higher up as possible.
Diffstat (limited to 'pretyping/evarsolve.mli')
| -rw-r--r-- | pretyping/evarsolve.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 908adac7e4..74aee9da59 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -77,7 +77,7 @@ type conversion_check = unify_flags -> unification_kind -> - [c] does not contain any Meta(_) *) -val instantiate_evar : unifier -> unify_flags -> evar_map -> +val instantiate_evar : unifier -> unify_flags -> env -> evar_map -> Evar.t -> constr -> evar_map (** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]), @@ -125,7 +125,7 @@ exception IllTypedInstance of env * types * types (* May raise IllTypedInstance if types are not convertible *) val check_evar_instance : unifier -> unify_flags -> - evar_map -> Evar.t -> constr -> evar_map + env -> evar_map -> Evar.t -> constr -> evar_map val remove_instance_local_defs : evar_map -> Evar.t -> 'a array -> 'a list |