Merge PR #6047: A generic printer for ltac values

26 files changed, 477 insertions, 181 deletions

diff --git a/API/API.mli b/API/API.mli
index e207930771..589745b616 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4973,10 +4973,23 @@ end
 
 module Genprint :
 sig
+  type printer_with_level =
+    { default_already_surrounded : Notation_term.tolerability;
+      default_ensure_surrounded : Notation_term.tolerability;
+      printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t }
+  type printer_result =
+    | PrinterBasic of (unit -> Pp.t)
+    | PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
+    | PrinterNeedsContextAndLevel of printer_with_level
   type 'a printer = 'a -> Pp.t
-  val generic_top_print : Genarg.tlevel Genarg.generic_argument printer
+  type 'a top_printer = 'a -> printer_result
   val register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type ->
-                        'raw printer -> 'glb printer -> 'top printer -> unit
+                        'raw printer -> 'glb printer -> 'top top_printer -> unit
+  val register_vernac_print0 : ('raw, 'glb, 'top) Genarg.genarg_type ->
+                        'raw printer -> unit
+  val register_val_print0 : 'top Geninterp.Val.typ -> 'top top_printer -> unit
+  val generic_top_print : Genarg.tlevel Genarg.generic_argument top_printer
+  val generic_val_print : Geninterp.Val.t top_printer
 end
 
 module Pputils :
@@ -4997,6 +5010,8 @@ sig
   val pr_name : Names.Name.t -> Pp.t
   [@@ocaml.deprecated "alias of API.Names.Name.print"]
 
+  val lsimpleconstr : Notation_term.tolerability
+  val ltop : Notation_term.tolerability
   val pr_id : Names.Id.t -> Pp.t
   val pr_or_var : ('a -> Pp.t) -> 'a Misctypes.or_var -> Pp.t
   val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t
@@ -5029,6 +5044,7 @@ sig
   val pr_constr_pattern : Pattern.constr_pattern -> Pp.t
   val pr_glob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t
   val pr_lglob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t
+  val pr_econstr_n_env : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> EConstr.constr -> Pp.t
   val pr_econstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
   val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t
   val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t
@@ -5041,6 +5057,7 @@ sig
   val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t
 
   val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t
+  val pr_closed_glob_n_env : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Ltac_pretype.closed_glob_constr -> Pp.t
   val pr_closed_glob_env : Environ.env -> Evd.evar_map -> Ltac_pretype.closed_glob_constr -> Pp.t
   val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.t
   val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.t
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 699ee6b840..5be8257e87 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -50,6 +50,13 @@ Some tactics and related functions now support static configurability, e.g.:
   - if None, tells to behave as told with the flag Keep Proof Equalities
   - if Some b, tells to keep proof equalities iff b is true
 
+Declaration of printers for arguments used only in vernac command
+
+- It should now use "declare_extra_vernac_genarg_pprule" rather than
+  "declare_extra_genarg_pprule", otherwise, a failure at runtime might
+  happen. An alternative is to register the corresponding argument as
+  a value, using "Geninterp.register_val0 wit None".
+
 ## Changes between Coq 8.6 and Coq 8.7
 
 ### Ocaml
diff --git a/engine/geninterp.ml b/engine/geninterp.ml
index e79e258fbc..2a1addcd3f 100644
--- a/engine/geninterp.ml
+++ b/engine/geninterp.ml
@@ -47,6 +47,8 @@ struct
 
 end
 
+module ValTMap = ValT.Map
+
 module ValReprObj =
 struct
   type ('raw, 'glb, 'top) obj = 'top Val.tag
diff --git a/engine/geninterp.mli b/engine/geninterp.mli
index 492e372adb..ae0b26e594 100644
--- a/engine/geninterp.mli
+++ b/engine/geninterp.mli
@@ -39,6 +39,10 @@ sig
   val inject : 'a tag -> 'a -> t
 
 end
+
+module ValTMap (M : Dyn.TParam) :
+  Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ
+
 (** Dynamic types for toplevel values. While the generic types permit to relate
     objects at various levels of interpretation, toplevel values are wearing
     their own type regardless of where they came from. This allows to use the
diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp
index 12b7b171b7..9742a002d7 100644
--- a/grammar/argextend.mlp
+++ b/grammar/argextend.mlp
@@ -186,12 +186,7 @@ let declare_vernac_argument loc s pr cl =
       value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) =
         Genarg.create_arg $se$ >>;
      make_extend loc s cl wit;
-    <:str_item< do {
-      Pptactic.declare_extra_genarg_pprule $wit$
-        $pr_rules$
-        (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not globwit printer."))
-        (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not wit printer.")) }
-      >> ]
+    <:str_item< Pptactic.declare_extra_vernac_genarg_pprule $wit$ $pr_rules$ >> ]
 
 open Pcaml
 
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp
index 536ee7ca56..c2d767396a 100644
--- a/grammar/q_util.mlp
+++ b/grammar/q_util.mlp
@@ -94,10 +94,14 @@ let coincide s pat off =
   done;
   !break
 
+let check_separator sep =
+  if sep <> "" then failwith "Separator is only for arguments with suffix _list_sep."
+
 let rec parse_user_entry s sep =
   let l = String.length s in
   if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
     let entry = parse_user_entry (String.sub s 3 (l-8)) "" in
+    check_separator sep;
     Ulist1 entry
   else if l > 12 && coincide s "ne_" 0 &&
                    coincide s "_list_sep" (l-9) then
@@ -105,16 +109,20 @@ let rec parse_user_entry s sep =
     Ulist1sep (entry, sep)
   else if l > 5 && coincide s "_list" (l-5) then
     let entry = parse_user_entry (String.sub s 0 (l-5)) "" in
+    check_separator sep;
     Ulist0 entry
   else if l > 9 && coincide s "_list_sep" (l-9) then
     let entry = parse_user_entry (String.sub s 0 (l-9)) "" in
     Ulist0sep (entry, sep)
   else if l > 4 && coincide s "_opt" (l-4) then
     let entry = parse_user_entry (String.sub s 0 (l-4)) "" in
+    check_separator sep;
     Uopt entry
   else if l = 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
     let n = Char.code s.[6] - 48 in
+    check_separator sep;
     Uentryl ("tactic", n)
   else
     let s = match s with "hyp" -> "var" | _ -> s in
+    check_separator sep;
     Uentry s
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 45dec5112b..65c55a584a 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -28,7 +28,7 @@ let wit_string : string uniform_genarg_type =
   make0 "string"
 
 let wit_pre_ident : string uniform_genarg_type =
-  make0 ~dyn:(val_tag (topwit wit_string)) "preident"
+  make0 "preident"
 
 let loc_of_or_by_notation f = function
   | AN c -> f c
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 6bd43455f6..e9f9709cb6 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -11,6 +11,26 @@ sig
   type 'a t
 end
 
+module type MapS =
+sig
+  type t
+  type 'a obj
+  type 'a key
+  val empty : t
+  val add : 'a key -> 'a obj -> t -> t
+  val remove : 'a key -> t -> t
+  val find : 'a key -> t -> 'a obj
+  val mem : 'a key -> t -> bool
+
+  type any = Any : 'a key * 'a obj -> any
+
+  type map = { map : 'a. 'a key -> 'a obj -> 'a obj }
+  val map : map -> t -> t
+
+  val iter : (any -> unit) -> t -> unit
+  val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
+end
+
 module type PreS =
 sig
 type 'a tag
@@ -24,24 +44,7 @@ type any = Any : 'a tag -> any
 
 val name : string -> any option
 
-module Map(M : TParam) :
-sig
-  type t
-  val empty : t
-  val add : 'a tag -> 'a M.t -> t -> t
-  val remove : 'a tag -> t -> t
-  val find : 'a tag -> t -> 'a M.t
-  val mem : 'a tag -> t -> bool
-
-  type any = Any : 'a tag * 'a M.t -> any
-
-  type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t }
-  val map : map -> t -> t
-
-  val iter : (any -> unit) -> t -> unit
-  val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
-
-end
+module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag
 
 val dump : unit -> (int * string) list
 
@@ -104,6 +107,8 @@ let dump () = Int.Map.bindings !dyntab
 module Map(M : TParam) =
 struct
 type t = Obj.t M.t Int.Map.t
+type 'a obj = 'a M.t
+type 'a key = 'a tag
 let cast : 'a M.t -> 'b M.t = Obj.magic
 let empty = Int.Map.empty
 let add tag v m = Int.Map.add tag (cast v) m
diff --git a/lib/dyn.mli b/lib/dyn.mli
index e43c8a9bcf..a2bbd95a78 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -13,6 +13,26 @@ sig
   type 'a t
 end
 
+module type MapS =
+sig
+  type t
+  type 'a obj
+  type 'a key
+  val empty : t
+  val add : 'a key -> 'a obj -> t -> t
+  val remove : 'a key -> t -> t
+  val find : 'a key -> t -> 'a obj
+  val mem : 'a key -> t -> bool
+
+  type any = Any : 'a key * 'a obj -> any
+
+  type map = { map : 'a. 'a key -> 'a obj -> 'a obj }
+  val map : map -> t -> t
+
+  val iter : (any -> unit) -> t -> unit
+  val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
+end
+
 module type S =
 sig
 type 'a tag
@@ -26,24 +46,7 @@ type any = Any : 'a tag -> any
 
 val name : string -> any option
 
-module Map(M : TParam) :
-sig
-  type t
-  val empty : t
-  val add : 'a tag -> 'a M.t -> t -> t
-  val remove : 'a tag -> t -> t
-  val find : 'a tag -> t -> 'a M.t
-  val mem : 'a tag -> t -> bool
-
-  type any = Any : 'a tag * 'a M.t -> any
-
-  type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t }
-  val map : map -> t -> t
-
-  val iter : (any -> unit) -> t -> unit
-  val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
-
-end
+module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag
 
 val dump : unit -> (int * string) list
 
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 62ecaa552b..829556a71e 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -144,8 +144,7 @@ END
 
 let () =
   let raw_printer _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in
-  let printer _ _ _ _ = str "<Unavailable printer for rec_definition>" in
-  Pptactic.declare_extra_genarg_pprule wit_function_rec_definition_loc raw_printer printer printer
+  Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer
 
 (* TASSI: n'importe quoi ! *)
 VERNAC COMMAND EXTEND Function
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index 1a2d895868..fea9e837b1 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -155,6 +155,4 @@ let () =
   | None -> mt ()
   | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac
   in
-  (* should not happen *)
-  let dummy _ _ _ expr = assert false in
-  Pptactic.declare_extra_genarg_pprule wit_withtac printer dummy dummy
+  Pptactic.declare_extra_vernac_genarg_pprule wit_withtac printer
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index c22e683235..b148d962ed 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -195,8 +195,7 @@ let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wi
 
 let () =
   let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in
-  let printer _ _ _ _ = Pp.str "<Unavailable printer for binders>" in
-  Pptactic.declare_extra_genarg_pprule wit_binders raw_printer printer printer
+  Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer
 
 open Pcoq
 
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index d588c888c4..e467d3e2ca 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -116,7 +116,13 @@ type 'a extra_genarg_printer =
         | Val.Base t ->
           begin match Val.eq t tag with
           | None -> default
-          | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x)
+          | Some Refl ->
+             let open Genprint in
+             match generic_top_print (in_gen (Topwit wit) x) with
+             | PrinterBasic pr -> pr ()
+             | PrinterNeedsContext pr -> pr (Global.env()) Evd.empty
+             | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+                printer (Global.env()) Evd.empty default_ensure_surrounded
           end
         | _ -> default
 
@@ -432,12 +438,13 @@ type 'a extra_genarg_printer =
       let pr_occs = pr_with_occurrences (fun () -> str" |- *") (occs,()) in
       (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs)
 
-  let pr_clauses default_is_concl pr_id = function
+  (* Some true = default is concl; Some false = default is all; None = no default *)
+  let pr_clauses has_default pr_id = function
     | { onhyps=Some []; concl_occs=occs }
-        when (match default_is_concl with Some true -> true | _ -> false) ->
+        when (match has_default with Some true -> true | _ -> false) ->
       pr_with_occurrences mt (occs,())
     | { onhyps=None; concl_occs=AllOccurrences }
-        when (match default_is_concl with Some false -> true | _ -> false) -> mt ()
+        when (match has_default with Some false -> true | _ -> false) -> mt ()
     | { onhyps=None; concl_occs=NoOccurrences } ->
       pr_in (str " * |-")
     | { onhyps=None; concl_occs=occs } ->
@@ -1174,83 +1181,122 @@ let declare_extra_genarg_pprule wit
     g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x
   in
   let h x =
-    let env = Global.env () in
-    h (pr_econstr_env env Evd.empty) (pr_leconstr_env env Evd.empty) (fun _ _ -> str "<tactic>") x
+    Genprint.PrinterNeedsContext (fun env sigma ->
+        h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") x)
   in
   Genprint.register_print0 wit f g h
 
+let declare_extra_vernac_genarg_pprule wit f =
+  let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in
+  Genprint.register_vernac_print0 wit f
+
 (** Registering *)
 
-let run_delayed c = c (Global.env ()) Evd.empty
+let pr_intro_pattern_env p = Genprint.PrinterNeedsContext (fun env sigma ->
+  let print_constr c = let (sigma, c) = c env sigma in pr_econstr_env env sigma c in
+  Miscprint.pr_intro_pattern print_constr p)
+
+let pr_red_expr_env r = Genprint.PrinterNeedsContext (fun env sigma ->
+  pr_red_expr (pr_econstr_env env sigma, pr_leconstr_env env sigma,
+               pr_evaluable_reference_env env, pr_constr_pattern_env env sigma) r)
+
+let pr_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma ->
+  let sigma, bl = bl env sigma in
+  Miscprint.pr_bindings
+    (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl)
+
+let pr_with_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma ->
+  let sigma, bl = bl env sigma in
+  pr_with_bindings
+    (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl)
+
+let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma ->
+  let sigma, c = match c with
+  | clear_flag,ElimOnConstr g -> let sigma,c = g env sigma in sigma,(clear_flag,ElimOnConstr c)
+  | clear_flag,ElimOnAnonHyp n as x -> sigma, x
+  | clear_flag,ElimOnIdent id as x -> sigma, x in
+  pr_destruction_arg
+    (pr_econstr_env env sigma) (pr_leconstr_env env sigma) c)
+
+let make_constr_printer f c =
+  Genprint.PrinterNeedsContextAndLevel {
+      Genprint.default_already_surrounded = Ppconstr.ltop;
+      Genprint.default_ensure_surrounded = Ppconstr.lsimpleconstr;
+      Genprint.printer = (fun env sigma n -> f env sigma n c)}
 
-let run_delayed_destruction_arg = function (* HH: Using Evd.empty looks suspicious *)
-  | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (snd (run_delayed g))
-  | clear_flag,ElimOnAnonHyp n as x -> x
-  | clear_flag,ElimOnIdent id as x -> x
+let lift f a = Genprint.PrinterBasic (fun () -> f a)
 
 let () =
   let pr_bool b = if b then str "true" else str "false" in
   let pr_unit _ = str "()" in
-  let pr_string s = str "\"" ++ str s ++ str "\"" in
   Genprint.register_print0 wit_int_or_var
-    (pr_or_var int) (pr_or_var int) int;
+    (pr_or_var int) (pr_or_var int) (lift int);
   Genprint.register_print0 wit_ref
-    pr_reference (pr_or_var (pr_located pr_global)) pr_global;
+    pr_reference (pr_or_var (pr_located pr_global)) (lift pr_global);
   Genprint.register_print0 wit_ident
-    pr_id pr_id pr_id;
+    pr_id pr_id (lift pr_id);
   Genprint.register_print0 wit_var
-    (pr_located pr_id) (pr_located pr_id) pr_id;
+    (pr_located pr_id) (pr_located pr_id) (lift pr_id);
   Genprint.register_print0
     wit_intro_pattern
     (Miscprint.pr_intro_pattern pr_constr_expr)
     (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c))
-    (Miscprint.pr_intro_pattern (fun c -> pr_econstr (snd (run_delayed c))));
+    pr_intro_pattern_env;
   Genprint.register_print0
     wit_clause_dft_concl
     (pr_clauses (Some true) pr_lident)
     (pr_clauses (Some true) pr_lident)
-    (pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)))
+    (fun c -> Genprint.PrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c))
   ;
   Genprint.register_print0
     wit_constr
     Ppconstr.pr_constr_expr
     (fun (c, _) -> Printer.pr_glob_constr c)
-    Printer.pr_econstr
+    (make_constr_printer Printer.pr_econstr_n_env)
   ;
   Genprint.register_print0
     wit_uconstr
     Ppconstr.pr_constr_expr
     (fun (c,_) -> Printer.pr_glob_constr c)
-    Printer.pr_closed_glob
+    (make_constr_printer Printer.pr_closed_glob_n_env)
   ;
   Genprint.register_print0
     wit_open_constr
     Ppconstr.pr_constr_expr
     (fun (c, _) -> Printer.pr_glob_constr c)
-    Printer.pr_econstr
+    (make_constr_printer Printer.pr_econstr_n_env)
   ;
   Genprint.register_print0 wit_red_expr
     (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))
     (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr))
-    (pr_red_expr (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern));
-  Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
+    pr_red_expr_env
+  ;
+  Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift pr_quantified_hypothesis);
   Genprint.register_print0 wit_bindings
     (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
     (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun it -> Miscprint.pr_bindings_no_with pr_econstr pr_leconstr (snd (run_delayed it)));
+    pr_bindings_env
+  ;
   Genprint.register_print0 wit_constr_with_bindings
     (pr_with_bindings pr_constr_expr pr_lconstr_expr)
     (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun it -> pr_with_bindings pr_econstr pr_leconstr (snd (run_delayed it)));
+    pr_with_bindings_env
+  ;
+  Genprint.register_print0 wit_open_constr_with_bindings
+    (pr_with_bindings pr_constr_expr pr_lconstr_expr)
+    (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+    pr_with_bindings_env
+  ;
   Genprint.register_print0 Tacarg.wit_destruction_arg
     (pr_destruction_arg pr_constr_expr pr_lconstr_expr)
     (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun it -> pr_destruction_arg pr_econstr pr_leconstr (run_delayed_destruction_arg it));
-  Genprint.register_print0 Stdarg.wit_int int int int;
-  Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool;
-  Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit;
-  Genprint.register_print0 Stdarg.wit_pre_ident str str str;
-  Genprint.register_print0 Stdarg.wit_string pr_string pr_string pr_string
+    pr_destruction_arg_env
+  ;
+  Genprint.register_print0 Stdarg.wit_int int int (lift int);
+  Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool (lift pr_bool);
+  Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit (lift pr_unit);
+  Genprint.register_print0 Stdarg.wit_pre_ident str str (lift str);
+  Genprint.register_print0 Stdarg.wit_string qstring qstring (lift qstring)
 
 let () =
   let printer _ _ prtac = prtac (0, E) in
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index d9da954fe6..5ecfaf590c 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -46,6 +46,10 @@ val declare_extra_genarg_pprule :
   'b glob_extra_genarg_printer ->
   'c extra_genarg_printer -> unit
 
+val declare_extra_vernac_genarg_pprule :
+  ('a, 'b, 'c) genarg_type ->
+  'a raw_extra_genarg_printer -> unit
+
 type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
 
 type pp_tactic = {
@@ -69,11 +73,16 @@ val pr_may_eval :
 val pr_and_short_name : ('a -> Pp.t) -> 'a and_short_name -> Pp.t
 val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t
 
+val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t
+
+val pr_quantified_hypothesis : quantified_hypothesis -> Pp.t
+
 val pr_in_clause :
   ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t
 
-val pr_clauses :  bool option ->
+val pr_clauses : (* default: *) bool option ->
   ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t
+  (* Some true = default is concl; Some false = default is all; None = no default *)
 
 val pr_raw_generic : env -> rlevel generic_argument -> Pp.t
 
@@ -116,3 +125,6 @@ val pr_value : tolerability -> Val.t -> Pp.t
 
 
 val ltop : tolerability
+
+val make_constr_printer : (env -> Evd.evar_map -> Notation_term.tolerability -> 'a -> Pp.t) ->
+  'a Genprint.top_printer
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index a79a92a661..4d171ecbc2 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -17,15 +17,23 @@ open Geninterp
 
 exception CannotCoerceTo of string
 
+let base_val_typ wit =
+  match val_tag (topwit wit) with Val.Base t -> t | _ -> CErrors.anomaly (Pp.str "Not a base val.")
+
 let (wit_constr_context : (Empty.t, Empty.t, EConstr.constr) Genarg.genarg_type) =
   let wit = Genarg.create_arg "constr_context" in
   let () = register_val0 wit None in
+  let () = Genprint.register_val_print0 (base_val_typ wit)
+    (Pptactic.make_constr_printer Printer.pr_econstr_n_env) in
   wit
 
 (* includes idents known to be bound and references *)
 let (wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) Genarg.genarg_type) =
   let wit = Genarg.create_arg "constr_under_binders" in
   let () = register_val0 wit None in
+  let () = Genprint.register_val_print0 (base_val_typ wit)
+             (fun c ->
+               Genprint.PrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in
   wit
 
 (** All the types considered here are base types *)
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 0bf6e3d155..ee84be5414 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -63,28 +63,37 @@ let get_separator = function
 | None -> user_err Pp.(str "Missing separator.")
 | Some sep -> sep
 
-let rec parse_user_entry s sep =
+let check_separator ?loc = function
+| None -> ()
+| Some _ -> user_err ?loc (str "Separator is only for arguments with suffix _list_sep.")
+
+let rec parse_user_entry ?loc s sep =
   let l = String.length s in
   if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
-    let entry = parse_user_entry (String.sub s 3 (l-8)) None in
+    let entry = parse_user_entry ?loc (String.sub s 3 (l-8)) None in
+    check_separator ?loc sep;
     Ulist1 entry
   else if l > 12 && coincide s "ne_" 0 &&
                    coincide s "_list_sep" (l-9) then
-    let entry = parse_user_entry (String.sub s 3 (l-12)) None in
+    let entry = parse_user_entry ?loc (String.sub s 3 (l-12)) None in
     Ulist1sep (entry, get_separator sep)
   else if l > 5 && coincide s "_list" (l-5) then
-    let entry = parse_user_entry (String.sub s 0 (l-5)) None in
+    let entry = parse_user_entry ?loc (String.sub s 0 (l-5)) None in
+    check_separator ?loc sep;
     Ulist0 entry
   else if l > 9 && coincide s "_list_sep" (l-9) then
-    let entry = parse_user_entry (String.sub s 0 (l-9)) None in
+    let entry = parse_user_entry ?loc (String.sub s 0 (l-9)) None in
     Ulist0sep (entry, get_separator sep)
   else if l > 4 && coincide s "_opt" (l-4) then
-    let entry = parse_user_entry (String.sub s 0 (l-4)) None in
+    let entry = parse_user_entry ?loc (String.sub s 0 (l-4)) None in
+    check_separator ?loc sep;
     Uopt entry
   else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
     let n = Char.code s.[6] - 48 in
+    check_separator ?loc sep;
     Uentryl ("tactic", n)
   else
+    let _ = check_separator ?loc sep in
     Uentry s
 
 let interp_entry_name interp symb =
@@ -203,7 +212,7 @@ let register_tactic_notation_entry name entry =
 let interp_prod_item = function
   | TacTerm s -> TacTerm s
   | TacNonTerm (loc, ((nt, sep), ido)) ->
-    let symbol = parse_user_entry nt sep in
+    let symbol = parse_user_entry ?loc nt sep in
     let interp s = function
     | None ->
       if String.Map.mem s !entry_names then String.Map.find s !entry_names
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 66f124d2d1..fd75862c6f 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -76,6 +76,9 @@ let out_gen wit v =
 
 let val_tag wit = val_tag (topwit wit)
 
+let base_val_typ wit =
+  match val_tag wit with Val.Base t -> t | _ -> anomaly (str "Not a base val.")
+
 let pr_argument_type arg =
   let Val.Dyn (tag, _) = arg in
   Val.pr tag
@@ -124,6 +127,8 @@ type tacvalue =
 let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
   let wit = Genarg.create_arg "tacvalue" in
   let () = register_val0 wit None in
+  let () = Genprint.register_val_print0 (base_val_typ wit)
+             (fun _ -> Genprint.PrinterBasic (fun () -> str "<tactic closure>")) in
   wit
 
 let of_tacvalue v = in_gen (topwit wit_tacvalue) v
@@ -231,24 +236,16 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with
 (* Displays a value *)
 let pr_value env v =
   let v = Value.normalize v in
-  if has_type v (topwit wit_tacvalue) then str "a tactic"
-  else if has_type v (topwit wit_constr_context) then
-    let c = out_gen (topwit wit_constr_context) v in
-    match env with
-    | Some (env,sigma) -> pr_leconstr_env env sigma c
-    | _ -> str "a term"
-  else if has_type v (topwit wit_constr) then
-    let c = out_gen (topwit wit_constr) v in
+  let pr_with_env pr =
     match env with
-    | Some (env,sigma) -> pr_leconstr_env env sigma c
-    | _ -> str "a term"
-  else if has_type v (topwit wit_constr_under_binders) then
-    let c = out_gen (topwit wit_constr_under_binders) v in
-    match env with
-    | Some (env,sigma) -> pr_lconstr_under_binders_env env sigma c
-    | _ -> str "a term"
-  else
-    str "a value of type" ++ spc () ++ pr_argument_type v
+    | Some (env,sigma) -> pr env sigma
+    | None -> str "a value of type" ++ spc () ++ pr_argument_type v in
+  let open Genprint in
+  match generic_val_print v with
+  | PrinterBasic pr -> pr ()
+  | PrinterNeedsContext pr -> pr_with_env pr
+  | PrinterNeedsContextAndLevel { default_already_surrounded; printer } ->
+     pr_with_env (fun env sigma -> printer env sigma default_already_surrounded)
 
 let pr_closure env ist body =
   let pp_body = Pptactic.pr_glob_tactic env body in
@@ -818,51 +815,16 @@ let interp_constr_may_eval ist env sigma c =
   end
 
 (** TODO: should use dedicated printers *)
-let rec message_of_value v =
+let message_of_value v =
   let v = Value.normalize v in
-  let open Ftactic in
-  if has_type v (topwit wit_tacvalue) then
-    Ftactic.return (str "<tactic>")
-  else if has_type v (topwit wit_constr) then
-    let v = out_gen (topwit wit_constr) v in
-    Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end
-  else if has_type v (topwit wit_constr_under_binders) then
-    let c = out_gen (topwit wit_constr_under_binders) v in
-    Ftactic.enter begin fun gl ->
-      Ftactic.return (pr_constr_under_binders_env (pf_env gl) (project gl) c)
-    end
-  else if has_type v (topwit wit_unit) then
-    Ftactic.return (str "()")
-  else if has_type v (topwit wit_int) then
-    Ftactic.return (int (out_gen (topwit wit_int) v))
-  else if has_type v (topwit wit_intro_pattern) then
-    let p = out_gen (topwit wit_intro_pattern) v in
-    let print env sigma c =
-      let (sigma, c) = c env sigma in
-      pr_econstr_env env sigma c
-    in
-    Ftactic.enter begin fun gl ->
-      Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (project gl) c) p)
-    end
-  else if has_type v (topwit wit_constr_context) then
-    let c = out_gen (topwit wit_constr_context) v in
-    Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end
-  else if has_type v (topwit wit_uconstr) then
-    let c = out_gen (topwit wit_uconstr) v in
-    Ftactic.enter begin fun gl ->
-      Ftactic.return (pr_closed_glob_env (pf_env gl)
-                        (project gl) c)
-    end
-  else if has_type v (topwit wit_var) then
-    let id = out_gen (topwit wit_var) v in
-    Ftactic.enter begin fun gl -> Ftactic.return (Id.print id) end
-  else match Value.to_list v with
-  | Some l ->
-    Ftactic.List.map message_of_value l >>= fun l ->
-    Ftactic.return (prlist_with_sep spc (fun x -> x) l)
-  | None ->
-    let tag = pr_argument_type v in
-    Ftactic.return (str "<" ++ tag ++ str ">") (** TODO *)
+  let pr_with_env pr =
+    Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in
+  let open Genprint in
+  match generic_val_print v with
+  | PrinterBasic pr -> Ftactic.return (pr ())
+  | PrinterNeedsContext pr -> pr_with_env pr
+  | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+     pr_with_env (fun env sigma -> printer env sigma default_ensure_surrounded)
 
 let interp_message_token ist = function
   | MsgString s -> Ftactic.return (str s)
@@ -946,13 +908,13 @@ let interp_in_hyp_as ist env sigma (id,ipat) =
   let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in
   sigma,(interp_hyp ist env sigma id,ipat)
 
-let interp_binding_name ist sigma = function
+let interp_binding_name ist env sigma = function
   | AnonHyp n -> AnonHyp n
   | NamedHyp id ->
       (* If a name is bound, it has to be a quantified hypothesis *)
       (* user has to use other names for variables if these ones clash with *)
       (* a name intented to be used as a (non-variable) identifier *)
-      try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist None(Loc.tag id)
+      try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (Loc.tag id)
       with Not_found -> NamedHyp id
 
 let interp_declared_or_quantified_hypothesis ist env sigma = function
@@ -964,7 +926,7 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function
 
 let interp_binding ist env sigma (loc,(b,c)) =
   let sigma, c = interp_open_constr ist env sigma c in
-  sigma, (loc,(interp_binding_name ist sigma b,c))
+  sigma, (loc,(interp_binding_name ist env sigma b,c))
 
 let interp_bindings ist env sigma = function
 | NoBindings ->
@@ -1386,10 +1348,14 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
         end >>= fun v ->
         (* No errors happened, we propagate the trace *)
         let v = append_trace trace v in
-        Proofview.tclLIFT begin
-          debugging_step ist
-	    (fun () ->
-	      str"evaluation returns"++fnl()++pr_value None v)
+        let call_debug env =
+          Proofview.tclLIFT (debugging_step ist (fun () -> str"evaluation returns"++fnl()++pr_value env v)) in
+        begin
+          let open Genprint in
+          match generic_val_print v with
+          | PrinterBasic _ -> call_debug None
+          | PrinterNeedsContext _ | PrinterNeedsContextAndLevel _ ->
+             Proofview.Goal.enter (fun gl -> call_debug (Some (pf_env gl,project gl)))
         end <*>
         if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval
       else
diff --git a/printing/genprint.ml b/printing/genprint.ml
index 543b05024d..776a212b5c 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -8,13 +8,100 @@
 
 open Pp
 open Genarg
+open Geninterp
+
+(* We register printers at two levels:
+   - generic arguments for general printers
+   - generic values for printing ltac values *)
+
+(* Printing generic values *)
+
+type printer_with_level =
+  { default_already_surrounded : Notation_term.tolerability;
+    default_ensure_surrounded : Notation_term.tolerability;
+    printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t }
+
+type printer_result =
+| PrinterBasic of (unit -> Pp.t)
+| PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
+| PrinterNeedsContextAndLevel of printer_with_level
 
 type 'a printer = 'a -> Pp.t
 
+type 'a top_printer = 'a -> printer_result
+
+module ValMap = ValTMap (struct type 'a t = 'a -> printer_result end)
+
+let print0_val_map = ref ValMap.empty
+
+let find_print_val_fun tag =
+  try ValMap.find tag !print0_val_map
+  with Not_found ->
+    let msg s = Pp.(str "print function not found for a value interpreted as " ++ str s ++ str ".") in
+    CErrors.anomaly (msg (Val.repr tag))
+
+let generic_val_print v =
+  let Val.Dyn (tag,v) = v in
+  find_print_val_fun tag v
+
+let register_val_print0 s pr =
+  print0_val_map := ValMap.add s pr !print0_val_map
+
+let combine_dont_needs pr_pair pr1 = function
+  | PrinterBasic pr2 ->
+     PrinterBasic (fun () -> pr_pair (pr1 ()) (pr2 ()))
+  | PrinterNeedsContext pr2 ->
+     PrinterNeedsContext (fun env sigma ->
+         pr_pair (pr1 ()) (pr2 env sigma))
+  | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+     PrinterNeedsContext (fun env sigma ->
+         pr_pair (pr1 ()) (printer env sigma default_ensure_surrounded))
+
+let combine_needs pr_pair pr1 = function
+  | PrinterBasic pr2 ->
+     PrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (pr2 ()))
+  | PrinterNeedsContext pr2 ->
+     PrinterNeedsContext (fun env sigma ->
+         pr_pair (pr1 env sigma) (pr2 env sigma))
+  | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+     PrinterNeedsContext (fun env sigma ->
+         pr_pair (pr1 env sigma) (printer env sigma default_ensure_surrounded))
+
+let combine pr_pair pr1 v2 =
+  match pr1 with
+  | PrinterBasic pr1 ->
+     combine_dont_needs pr_pair pr1 (generic_val_print v2)
+  | PrinterNeedsContext pr1 ->
+     combine_needs pr_pair pr1 (generic_val_print v2)
+  | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+     combine_needs pr_pair (fun env sigma -> printer env sigma default_ensure_surrounded)
+       (generic_val_print v2)
+
+let _ =
+  let pr_cons a b = Pp.(a ++ spc () ++ b) in
+  register_val_print0 Val.typ_list
+    (function
+     | [] -> PrinterBasic mt
+     | a::l ->
+        List.fold_left (combine pr_cons) (generic_val_print a) l)
+
+let _ =
+  register_val_print0 Val.typ_opt
+    (function
+     | None -> PrinterBasic Pp.mt
+     | Some v -> generic_val_print v)
+
+let _ =
+  let pr_pair a b = Pp.(a ++ spc () ++ b) in
+  register_val_print0 Val.typ_pair
+    (fun (v1,v2) -> combine pr_pair (generic_val_print v1) v2)
+
+(* Printing generic arguments *)
+
 type ('raw, 'glb, 'top) genprinter = {
   raw : 'raw printer;
   glb : 'glb printer;
-  top : 'top printer;
+  top : 'top -> printer_result;
 }
 
 module PrintObj =
@@ -27,7 +114,7 @@ struct
     let printer = {
       raw = (fun _ -> str "<genarg:" ++ str name ++ str ">");
       glb = (fun _ -> str "<genarg:" ++ str name ++ str ">");
-      top = (fun _ -> str "<genarg:" ++ str name ++ str ">");
+      top = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">"));
     } in
     Some printer
   | _ -> assert false
@@ -37,6 +124,18 @@ module Print = Register (PrintObj)
 
 let register_print0 wit raw glb top =
   let printer = { raw; glb; top; } in
+  Print.register0 wit printer;
+  match val_tag (Topwit wit), wit with
+  | Val.Base t, ExtraArg t' when Geninterp.Val.repr t = ArgT.repr t' ->
+     register_val_print0 t top
+  | _ ->
+     (* An alias, thus no primitive printer attached *)
+     ()
+
+let register_vernac_print0 wit raw =
+  let glb _ = CErrors.anomaly (Pp.str "vernac argument needs not globwit printer.") in
+  let top _ = CErrors.anomaly (Pp.str "vernac argument needs not wit printer.") in
+  let printer = { raw; glb; top; } in
   Print.register0 wit printer
 
 let raw_print wit v = (Print.obj wit).raw v
diff --git a/printing/genprint.mli b/printing/genprint.mli
index 130a89c929..2da9bbc36b 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -10,20 +10,37 @@
 
 open Genarg
 
+type printer_with_level =
+  { default_already_surrounded : Notation_term.tolerability;
+    default_ensure_surrounded : Notation_term.tolerability;
+    printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t }
+
+type printer_result =
+| PrinterBasic of (unit -> Pp.t)
+| PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
+| PrinterNeedsContextAndLevel of printer_with_level
+
 type 'a printer = 'a -> Pp.t
 
-val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw -> Pp.t
+type 'a top_printer = 'a -> printer_result
+
+val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw printer
 (** Printer for raw level generic arguments. *)
 
-val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> Pp.t
+val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb printer
 (** Printer for glob level generic arguments. *)
 
-val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> Pp.t
+val top_print : ('raw, 'glb, 'top) genarg_type -> 'top top_printer
 (** Printer for top level generic arguments. *)
 
+val register_print0 : ('raw, 'glb, 'top) genarg_type ->
+  'raw printer -> 'glb printer -> ('top -> printer_result) -> unit
+val register_val_print0 : 'top Geninterp.Val.typ ->
+  'top top_printer -> unit
+val register_vernac_print0 : ('raw, 'glb, 'top) genarg_type ->
+  'raw printer -> unit
+
 val generic_raw_print : rlevel generic_argument printer
 val generic_glb_print : glevel generic_argument printer
-val generic_top_print : tlevel generic_argument printer
-
-val register_print0 : ('raw, 'glb, 'top) genarg_type ->
-  'raw printer -> 'glb printer -> 'top printer -> unit
+val generic_top_print : tlevel generic_argument top_printer
+val generic_val_print : Geninterp.Val.t top_printer
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 102c6ef6de..109a40a037 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -738,34 +738,40 @@ let tag_var = tag Tag.variable
     pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
   }
 
-  type precedence =  Notation_term.precedence * Notation_term.parenRelation
   let modular_constr_pr = pr
   let rec fix rf x = rf (fix rf) x
   let pr = fix modular_constr_pr mt
 
+  let pr prec = function
+    (* A toplevel printer hack mimicking parsing, incidentally meaning
+       that we cannot use [pr] correctly anymore in a recursive loop
+       if the current expr is followed by other exprs which would be
+       interpreted as arguments *)
+    | { CAst.v = CAppExpl ((None,f,us),[]) } -> str "@" ++ pr_cref f us
+    | c -> pr prec c
+
   let transf env c =
     if !Flags.beautify_file then
       let r = Constrintern.for_grammar (Constrintern.intern_constr env) c in
       Constrextern.extern_glob_constr (Termops.vars_of_env env) r
     else c
 
-  let pr prec c = pr prec (transf (Global.env()) c)
+  let pr_expr prec c = pr prec (transf (Global.env()) c)
 
-  let pr_simpleconstr = function
-    | { CAst.v = CAppExpl ((None,f,us),[]) } -> str "@" ++ pr_cref f us
-    | c -> pr lsimpleconstr c
+  let pr_simpleconstr = pr_expr lsimpleconstr
 
   let default_term_pr = {
     pr_constr_expr   = pr_simpleconstr;
-    pr_lconstr_expr  = pr ltop;
+    pr_lconstr_expr  = pr_expr ltop;
     pr_constr_pattern_expr  = pr_simpleconstr;
-    pr_lconstr_pattern_expr = pr ltop
+    pr_lconstr_pattern_expr = pr_expr ltop
   }
 
   let term_pr = ref default_term_pr
 
   let set_term_pr = (:=) term_pr
 
+  let pr_constr_expr_n n c = pr_expr n c
   let pr_constr_expr c   = !term_pr.pr_constr_expr   c
   let pr_lconstr_expr c  = !term_pr.pr_lconstr_expr  c
   let pr_constr_pattern_expr c  = !term_pr.pr_constr_pattern_expr  c
@@ -775,5 +781,5 @@ let tag_var = tag Tag.variable
 
   let pr_record_body = pr_record_body_gen pr
 
-  let pr_binders = pr_undelimited_binders spc (pr ltop)
+  let pr_binders = pr_undelimited_binders spc (pr_expr ltop)
 
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 7546c748d8..be96cfce50 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -60,6 +60,7 @@ val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
 val pr_constr_expr : constr_expr -> Pp.t
 val pr_lconstr_expr : constr_expr -> Pp.t
 val pr_cases_pattern_expr : cases_pattern_expr -> Pp.t
+val pr_constr_expr_n : tolerability -> constr_expr -> Pp.t
 
 type term_pr = {
   pr_constr_expr   : constr_expr -> Pp.t;
@@ -86,9 +87,8 @@ val default_term_pr : term_pr
   Which has the same type. We can turn a modular printer into a printer by
   taking its fixpoint. *)
 
-type precedence
-val lsimpleconstr : precedence
-val ltop : precedence
+val lsimpleconstr : tolerability
+val ltop : tolerability
 val modular_constr_pr :
-  ((unit->Pp.t) -> precedence -> constr_expr -> Pp.t) ->
-  (unit->Pp.t) -> precedence  -> constr_expr -> Pp.t
+  ((unit->Pp.t) -> tolerability -> constr_expr -> Pp.t) ->
+  (unit->Pp.t) -> tolerability -> constr_expr -> Pp.t
diff --git a/printing/printer.ml b/printing/printer.ml
index 28b10c7812..c6650ea3b8 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -79,11 +79,14 @@ let _ =
    and only names of goal/section variables and rel names that do
    _not_ occur in the scope of the binder to be printed are avoided. *)
 
+let pr_econstr_n_core goal_concl_style env sigma n t =
+  pr_constr_expr_n n (extern_constr goal_concl_style env sigma t)
 let pr_econstr_core goal_concl_style env sigma t =
   pr_constr_expr (extern_constr goal_concl_style env sigma t)
 let pr_leconstr_core goal_concl_style env sigma t =
   pr_lconstr_expr (extern_constr goal_concl_style env sigma t)
 
+let pr_constr_n_env env sigma n c = pr_econstr_n_core false env sigma n (EConstr.of_constr c)
 let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c)
 let pr_constr_env env sigma c = pr_econstr_core false env sigma (EConstr.of_constr c)
 let _ = Hook.set Refine.pr_constr pr_constr_env
@@ -94,6 +97,7 @@ let pr_constr_goal_style_env env sigma c = pr_econstr_core true env sigma (ECons
 let pr_open_lconstr_env env sigma (_,c) = pr_lconstr_env env sigma c
 let pr_open_constr_env env sigma (_,c) = pr_constr_env env sigma c
 
+let pr_econstr_n_env env sigma c = pr_econstr_n_core false env sigma c
 let pr_leconstr_env env sigma c = pr_leconstr_core false env sigma c
 let pr_econstr_env env sigma c = pr_econstr_core false env sigma c
 
@@ -166,6 +170,8 @@ let pr_glob_constr c =
   let (sigma, env) = get_current_context () in
   pr_glob_constr_env env c
 
+let pr_closed_glob_n_env env sigma n c =
+  pr_constr_expr_n n (extern_closed_glob false env sigma c)
 let pr_closed_glob_env env sigma c =
   pr_constr_expr (extern_closed_glob false env sigma c)
 let pr_closed_glob c =
diff --git a/printing/printer.mli b/printing/printer.mli
index ba849bee6a..658ea6060b 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -33,6 +33,8 @@ val pr_constr_env          : env -> evar_map -> constr -> Pp.t
 val pr_constr              : constr -> Pp.t
 val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t
 
+val pr_constr_n_env        : env -> evar_map -> Notation_term.tolerability -> constr -> Pp.t
+
 (** Same, but resilient to [Nametab] errors. Prints fully-qualified
     names when [shortest_qualid_of_global] has failed. Prints "??"
     in case of remaining issues (such as reference not in env). *)
@@ -48,6 +50,8 @@ val pr_econstr         : EConstr.t -> Pp.t
 val pr_leconstr_env     : env -> evar_map -> EConstr.t -> Pp.t
 val pr_leconstr         : EConstr.t -> Pp.t
 
+val pr_econstr_n_env    : env -> evar_map -> Notation_term.tolerability -> EConstr.t -> Pp.t
+
 val pr_etype_env           : env -> evar_map -> EConstr.types -> Pp.t
 val pr_letype_env           : env -> evar_map -> EConstr.types -> Pp.t
 
@@ -70,6 +74,7 @@ val pr_ltype               : types -> Pp.t
 val pr_type_env            : env -> evar_map -> types -> Pp.t
 val pr_type                : types -> Pp.t
 
+val pr_closed_glob_n_env   : env -> evar_map -> Notation_term.tolerability -> closed_glob_constr -> Pp.t
 val pr_closed_glob_env     : env -> evar_map -> closed_glob_constr -> Pp.t
 val pr_closed_glob         : closed_glob_constr -> Pp.t
 
diff --git a/test-suite/bugs/closed/5786.v b/test-suite/bugs/closed/5786.v
new file mode 100644
index 0000000000..20301ec4f5
--- /dev/null
+++ b/test-suite/bugs/closed/5786.v
@@ -0,0 +1,29 @@
+(* Printing all kinds of Ltac generic arguments *)
+
+Tactic Notation "myidtac" string(v) := idtac v.
+Goal True.
+myidtac "foo".
+Abort.
+
+Tactic Notation "myidtac2" ref(c) := idtac c.
+Goal True.
+myidtac2 True.
+Abort.
+
+Tactic Notation "myidtac3" preident(s) := idtac s.
+Goal True.
+myidtac3 foo.
+Abort.
+
+Tactic Notation "myidtac4" int_or_var(n) := idtac n.
+Goal True.
+myidtac4 3.
+Abort.
+
+Tactic Notation "myidtac5" ident(id) := idtac id.
+Goal True.
+myidtac5 foo.
+Abort.
+
+
+
diff --git a/test-suite/output/idtac.out b/test-suite/output/idtac.out
new file mode 100644
index 0000000000..3855f88a72
--- /dev/null
+++ b/test-suite/output/idtac.out
@@ -0,0 +1,11 @@
+"foo"
+True
+foo
+3
+foo
+2
+< True False Prop >
+< True False Prop >
+<  >
+<  >
+<< 1 2 3 >>
diff --git a/test-suite/output/idtac.v b/test-suite/output/idtac.v
new file mode 100644
index 0000000000..ac60ea9175
--- /dev/null
+++ b/test-suite/output/idtac.v
@@ -0,0 +1,45 @@
+(* Printing all kinds of Ltac generic arguments *)
+
+Tactic Notation "myidtac" string(v) := idtac v.
+Goal True.
+myidtac "foo".
+Abort.
+
+Tactic Notation "myidtac2" ref(c) := idtac c.
+Goal True.
+myidtac2 True.
+Abort.
+
+Tactic Notation "myidtac3" preident(s) := idtac s.
+Goal True.
+myidtac3 foo.
+Abort.
+
+Tactic Notation "myidtac4" int_or_var(n) := idtac n.
+Goal True.
+myidtac4 3.
+Abort.
+
+Tactic Notation "myidtac5" ident(id) := idtac id.
+Goal True.
+myidtac5 foo.
+Abort.
+
+(* Checking non focussing of idtac for integers *)
+Goal True/\True. split.
+all:let c:=numgoals in idtac c.
+Abort.
+
+(* Checking printing of lists and its focussing *)
+Tactic Notation "myidtac6" constr_list(l) := idtac "<" l ">".
+Goal True/\True. split.
+all:myidtac6 True False Prop.
+(* An empty list is focussing because of interp_genarg of a constr *)
+(* even if it is not focussing on printing *)
+all:myidtac6.
+Abort.
+
+Tactic Notation "myidtac7" int_list(l) := idtac "<<" l ">>".
+Goal True/\True. split.
+all:myidtac7 1 2 3.
+Abort.