diff options
| author | Pierre-Marie Pédrot | 2019-03-20 15:04:02 +0100 |
|---|---|---|
| committer | GitHub | 2019-03-20 15:04:02 +0100 |
| commit | 6e6844e89bdf57f00bc1e4d3de110ca45d0b51bf (patch) | |
| tree | 20b7fa0a9f4f5f4c4ef8732c98b1c2349a9a2612 | |
| parent | 23b34aaaa4b990dbb9e924fbd32feda40c41edf8 (diff) | |
| parent | c5a6a100844803b2da370e4828655a9da377e624 (diff) | |
Merge pull request coq/ltac2#113 from maximedenes/printed-by-env
Adapt to changes in Coq's printers API
| -rw-r--r-- | src/tac2core.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index e5499f0c73..15fd625650 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -1184,8 +1184,8 @@ let () = GlobEnv.register_constr_interp0 wit_ltac2_quotation interp let () = - let pr_raw id = Genprint.PrinterBasic mt in - let pr_glb id = Genprint.PrinterBasic (fun () -> str "$" ++ Id.print id) in + let pr_raw id = Genprint.PrinterBasic (fun _env _sigma -> mt ()) in + let pr_glb id = Genprint.PrinterBasic (fun _env _sigma -> str "$" ++ Id.print id) in let pr_top _ = Genprint.TopPrinterBasic mt in Genprint.register_print0 wit_ltac2_quotation pr_raw pr_glb pr_top @@ -1209,8 +1209,8 @@ let () = Geninterp.register_interp0 wit_ltac2 interp let () = - let pr_raw _ = Genprint.PrinterBasic mt in - let pr_glb e = Genprint.PrinterBasic (fun () -> Tac2print.pr_glbexpr e) in + let pr_raw _ = Genprint.PrinterBasic (fun _env _sigma -> mt ()) in + let pr_glb e = Genprint.PrinterBasic (fun _env _sigma -> Tac2print.pr_glbexpr e) in let pr_top _ = Genprint.TopPrinterBasic mt in Genprint.register_print0 wit_ltac2 pr_raw pr_glb pr_top |