From 767816eece27e6bb8cba0bbf122507bd2a3b77a1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 1 Nov 2017 22:54:24 +0100
Subject: Using a specific function to register vernac printers.

---
 plugins/funind/g_indfun.ml4    | 3 +--
 plugins/ltac/g_obligations.ml4 | 4 +---
 plugins/ltac/g_rewrite.ml4     | 3 +--
 plugins/ltac/pptactic.ml       | 4 ++++
 plugins/ltac/pptactic.mli      | 4 ++++
 5 files changed, 11 insertions(+), 7 deletions(-)

(limited to 'plugins')

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 2c46b7624c..00ce94f6c1 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 058b205697..b47f07a453 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 = {
-- 
cgit v1.2.3