aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/tac2core.ml6
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 =