Fix printing of Ltac2 in quotations.

1 files changed, 6 insertions, 0 deletions

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 =