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 /vernac | |
| 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 '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 19ec0a3642..c8e308cb9c 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -605,7 +605,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 @@ -622,7 +622,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 604d1b28ff..d3bc06cd6c 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 && |