aboutsummaryrefslogtreecommitdiff
path: root/dev/dune
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-11-08 15:01:24 +0100
committerGaëtan Gilbert2018-11-08 15:01:24 +0100
commita7522a0ea76a6efaed9342d08a95363b56d88d32 (patch)
tree9ab8bd176949a072e0edb1f79502142cedcdb0b2 /dev/dune
parent108c15b51a7d5f647c8681fe7a37c86f0c5a8b9c (diff)
Remove checker printers
Now that the checker is using the regular kernel files it can also use the normal printers.
Diffstat (limited to 'dev/dune')
-rw-r--r--dev/dune11
1 files changed, 1 insertions, 10 deletions
diff --git a/dev/dune b/dev/dune
index fd6c8cf32c..bfa2d525c9 100644
--- a/dev/dune
+++ b/dev/dune
@@ -3,18 +3,9 @@
(public_name coq.top_printers)
(synopsis "Coq's Debug Printers")
(wrapped false)
- (modules :standard \ checker_printers)
+ (modules :standard)
(libraries coq.toplevel coq.plugins.ltac))
-(library
- (name checker_printers)
- (public_name coq.checker_printers)
- (synopsis "Coq's Debug Printers [for the Checker]")
- (wrapped false)
- (flags :standard -open Checklib)
- (modules checker_printers)
- (libraries coq.checklib))
-
(rule
(targets dune-dbg)
(deps dune-dbg.in