aboutsummaryrefslogtreecommitdiff
path: root/dev/dune
diff options
context:
space:
mode:
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