From 93e888000664191fa608a8fa0f8057bdda8fe084 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Aug 2017 22:51:37 +0200
Subject: Fix printing of Ltac2 in quotations.

---
 src/tac2core.ml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 7d18bf693e..95fd29ec33 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -806,6 +806,12 @@ let () =
   in
   Geninterp.register_interp0 wit_ltac2 interp
 
+let () =
+  let pr_raw _ = mt () in
+  let pr_glb e = Tac2print.pr_glbexpr e in
+  let pr_top _ = mt () in
+  Genprint.register_print0 wit_ltac2 pr_raw pr_glb pr_top
+
 (** Built-in notation scopes *)
 
 let add_scope s f =
-- 
cgit v1.2.3