diff options
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 11bb7a2341..b29af6680d 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -18,7 +18,7 @@ open Genarg open Geninterp open Stdarg open Libnames -open Notation_term +open Notation_gram open Misctypes open Locus open Decl_kinds @@ -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 @@ -515,6 +518,7 @@ let string_of_genarg_arg (ArgumentType arg) = else int i ++ str "-" ++ int j let pr_goal_selector toplevel = function + | SelectAlreadyFocused -> str "!:" | SelectNth i -> int i ++ str ":" | SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":" | SelectId id -> str "[" ++ Id.print id ++ str "]:" |