diff options
| author | Gaëtan Gilbert | 2019-12-31 20:06:08 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-12-31 20:06:08 +0100 |
| commit | 0b1f1f9e02f481613fda3d0e087a01cede15e65b (patch) | |
| tree | 9aa81047a428a19c3b19be3b6925b740e82aa339 /pretyping/evarsolve.mli | |
| parent | f1bcfcb3d62d4c0b709d70c82b40bf4d4e0b6c11 (diff) | |
| parent | 9d0e4b2ab78b89e39c63e8010ffd03745b309b5a (diff) | |
Merge PR #11338: Remove uses of Global in Evd API.
Reviewed-by: ejgallego
Reviewed-by: herbelin
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 |