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 /vernac | |
| 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 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 4 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 085689be0a..ba7ae5069b 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -606,7 +606,7 @@ let rec explain_evar_kind env sigma evk ty = let explain_typeclass_resolution env sigma evi k = match Typeclasses.class_of_constr env sigma evi.evar_concl with | Some _ -> - let env = Evd.evar_filtered_env evi in + let env = Evd.evar_filtered_env env evi in fnl () ++ str "Could not find an instance for " ++ pr_leconstr_env env sigma evi.evar_concl ++ pr_trailing_ne_context_of env sigma @@ -623,7 +623,7 @@ let explain_placeholder_kind env sigma c e = let explain_unsolvable_implicit env sigma evk explain = let evi = Evarutil.nf_evar_info sigma (Evd.find_undefined sigma evk) in - let env = Evd.evar_filtered_env evi in + let env = Evd.evar_filtered_env env evi in let type_of_hole = pr_leconstr_env env sigma evi.evar_concl in let pe = pr_trailing_ne_context_of env sigma in strbrk "Cannot infer " ++ diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 04f3e0d7b2..99d74f16cc 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -474,7 +474,7 @@ let program_inference_hook env sigma ev = let tac = !Obligations.default_tactic in let evi = Evd.find sigma ev in let evi = Evarutil.nf_evar_info sigma evi in - let env = Evd.evar_filtered_env evi in + let env = Evd.evar_filtered_env env evi in try let concl = evi.Evd.evar_concl in if not (Evarutil.is_ground_env sigma env && |