diff options
| author | Hugo Herbelin | 2017-11-24 19:00:13 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-24 19:00:13 +0100 |
| commit | 2bd31e5fffbd6722f20016c3962088ab2008e2c0 (patch) | |
| tree | 46f4b5a2d01cbaf88a3c1842bd78b056d1d385a2 | |
| parent | d0305718b4141aa08675743d4f85238301f37ad7 (diff) | |
A possible fix after PR#6158 (raw/glob generic printers for ltac values).
Can the printers exploit the ability to now take an environment?
| -rw-r--r-- | src/tac2core.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index e476da7259..48cec86540 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -987,9 +987,9 @@ let () = Pretyping.register_constr_interp0 wit_ltac2_quotation interp let () = - let pr_raw id = mt () in - let pr_glb id = str "$" ++ Id.print id in - let pr_top _ = Genprint.PrinterBasic mt in + let pr_raw id = Genprint.PrinterBasic mt in + let pr_glb id = Genprint.PrinterBasic (fun () -> str "$" ++ Id.print id) in + let pr_top _ = Genprint.TopPrinterBasic mt in Genprint.register_print0 wit_ltac2_quotation pr_raw pr_glb pr_top (** Ltac2 in Ltac1 *) @@ -1015,9 +1015,9 @@ let () = Geninterp.register_interp0 wit_ltac2 interp let () = - let pr_raw _ = mt () in - let pr_glb e = Tac2print.pr_glbexpr e in - let pr_top _ = Genprint.PrinterBasic mt in + let pr_raw _ = Genprint.PrinterBasic mt in + let pr_glb e = Genprint.PrinterBasic (fun () -> Tac2print.pr_glbexpr e) in + let pr_top _ = Genprint.TopPrinterBasic mt in Genprint.register_print0 wit_ltac2 pr_raw pr_glb pr_top (** Built-in notation scopes *) |