From 630bf63968c2b80d7fc46adb5e110281ef68f2e9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Apr 2016 21:53:40 +0200
Subject: Fixing printing of Function.

---
 plugins/funind/g_indfun.ml4 | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'plugins')

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index c63527deaf..aa9cc40234 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -162,6 +162,11 @@ GEXTEND Gram
 
 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
+
 (* TASSI: n'importe quoi ! *)
 VERNAC COMMAND EXTEND Function
    ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
-- 
cgit v1.2.3