diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2core.ml | 4 | ||||
| -rw-r--r-- | src/tac2env.ml | 2 |
2 files changed, 4 insertions, 2 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index ce53b781f5..e476da7259 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -989,7 +989,7 @@ let () = let () = let pr_raw id = mt () in let pr_glb id = str "$" ++ Id.print id in - let pr_top _ = mt () in + let pr_top _ = Genprint.PrinterBasic mt in Genprint.register_print0 wit_ltac2_quotation pr_raw pr_glb pr_top (** Ltac2 in Ltac1 *) @@ -1017,7 +1017,7 @@ let () = let () = let pr_raw _ = mt () in let pr_glb e = Tac2print.pr_glbexpr e in - let pr_top _ = mt () in + let pr_top _ = Genprint.PrinterBasic mt in Genprint.register_print0 wit_ltac2 pr_raw pr_glb pr_top (** Built-in notation scopes *) diff --git a/src/tac2env.ml b/src/tac2env.ml index 2f1124c156..d0f286b396 100644 --- a/src/tac2env.ml +++ b/src/tac2env.ml @@ -280,6 +280,8 @@ let std_prefix = let wit_ltac2 = Genarg.make0 "ltac2:value" let wit_ltac2_quotation = Genarg.make0 "ltac2:quotation" +let () = Geninterp.register_val0 wit_ltac2 None +let () = Geninterp.register_val0 wit_ltac2_quotation None let is_constructor qid = let (_, id) = repr_qualid qid in |