diff options
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 bd02d85d5..3dfe308a5 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 |