10 files changed, 29 insertions, 13 deletions

diff --git a/API/API.mli b/API/API.mli
index e20793077..608bd43cd 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4977,6 +4977,8 @@ sig
   val generic_top_print : Genarg.tlevel Genarg.generic_argument printer
   val register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type ->
                         'raw printer -> 'glb printer -> 'top printer -> unit
+  val register_vernac_print0 : ('raw, 'glb, 'top) Genarg.genarg_type ->
+                        'raw printer -> unit
 end
 
 module Pputils :
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 6ade6576f..b1ebec44e 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -38,6 +38,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/grammar/argextend.mlp b/grammar/argextend.mlp
index 12b7b171b..9742a002d 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/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 62ecaa552..829556a71 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 1a2d89586..fea9e837b 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 c22e68323..b148d962e 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 2c46b7624..00ce94f6c 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1180,6 +1180,10 @@ let declare_extra_genarg_pprule wit
   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
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 058b20569..b47f07a45 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 = {
diff --git a/printing/genprint.ml b/printing/genprint.ml
index 543b05024..b20ea0b62 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -39,6 +39,12 @@ let register_print0 wit raw glb top =
   let printer = { raw; glb; top; } in
   Print.register0 wit printer
 
+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
 let glb_print wit v = (Print.obj wit).glb v
 let top_print wit v = (Print.obj wit).top v
diff --git a/printing/genprint.mli b/printing/genprint.mli
index 130a89c92..76d80f3b5 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -27,3 +27,5 @@ val generic_top_print : tlevel generic_argument printer
 
 val register_print0 : ('raw, 'glb, 'top) genarg_type ->
   'raw printer -> 'glb printer -> 'top printer -> unit
+val register_vernac_print0 : ('raw, 'glb, 'top) genarg_type ->
+  'raw printer -> unit