From 2bd31e5fffbd6722f20016c3962088ab2008e2c0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 24 Nov 2017 19:00:13 +0100
Subject: A possible fix after PR#6158 (raw/glob generic printers for ltac
 values).

Can the printers exploit the ability to now take an environment?
---
 src/tac2core.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'src')

diff --git a/src/tac2core.ml b/src/tac2core.ml
index e476da7259..48cec86540 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -987,9 +987,9 @@ let () =
   Pretyping.register_constr_interp0 wit_ltac2_quotation interp
 
 let () =
-  let pr_raw id = mt () in
-  let pr_glb id = str "$" ++ Id.print id in
-  let pr_top _ = Genprint.PrinterBasic mt in
+  let pr_raw id = Genprint.PrinterBasic mt in
+  let pr_glb id = Genprint.PrinterBasic (fun () -> str "$" ++ Id.print id) in
+  let pr_top _ = Genprint.TopPrinterBasic mt in
   Genprint.register_print0 wit_ltac2_quotation pr_raw pr_glb pr_top
 
 (** Ltac2 in Ltac1 *)
@@ -1015,9 +1015,9 @@ let () =
   Geninterp.register_interp0 wit_ltac2 interp
 
 let () =
-  let pr_raw _ = mt () in
-  let pr_glb e = Tac2print.pr_glbexpr e in
-  let pr_top _ = Genprint.PrinterBasic mt in
+  let pr_raw _ = Genprint.PrinterBasic mt in
+  let pr_glb e = Genprint.PrinterBasic (fun () -> Tac2print.pr_glbexpr e) in
+  let pr_top _ = Genprint.TopPrinterBasic mt in
   Genprint.register_print0 wit_ltac2 pr_raw pr_glb pr_top
 
 (** Built-in notation scopes *)
-- 
cgit v1.2.3