diff options
| author | Hugo Herbelin | 2017-11-04 23:16:26 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-04 23:17:23 +0100 |
| commit | 57f479f13c869408f51fbebc744c3b67a07d7f7c (patch) | |
| tree | 39137fb151bcd494c435e511343d3f6318c80363 /src | |
| parent | 290e9585ac3b0f6ece3f1966457fef3811f88d10 (diff) | |
A possible fix after PR#6047 (a generic printer for ltac values).
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 |