diff options
| author | Maxime Dénès | 2018-05-03 17:44:34 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-05-25 14:55:49 +0200 |
| commit | dfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 (patch) | |
| tree | 33fdd7c2eb44e54e7777e2d074127b129c5385ac /plugins/ltac/pptactic.ml | |
| parent | d2533da244f770261478ae829167cb3a8ad38038 (diff) | |
Remove some occurrences of Evd.empty
We address the easy ones, but they should probably be all removed.
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index bd02d85d59..3dfe308a5d 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -149,9 +149,12 @@ let string_of_genarg_arg (ArgumentType arg) = let open Genprint in match generic_top_print (in_gen (Topwit wit) x) with | TopPrinterBasic pr -> pr () - | TopPrinterNeedsContext pr -> pr (Global.env()) Evd.empty + | TopPrinterNeedsContext pr -> + let env = Global.env() in + pr env (Evd.from_env env) | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> - printer (Global.env()) Evd.empty default_ensure_surrounded + let env = Global.env() in + printer env (Evd.from_env env) default_ensure_surrounded end | _ -> default |