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 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins/funind')

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
-- 
cgit v1.2.3