aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--parsing/dune5
1 files changed, 0 insertions, 5 deletions
diff --git a/parsing/dune b/parsing/dune
index b70612a52b..f931321358 100644
--- a/parsing/dune
+++ b/parsing/dune
@@ -5,11 +5,6 @@
(libraries proofs))
(rule
- (targets cLexer.ml)
- (deps (:ml4-file cLexer.ml4))
- (action (run camlp5o -loc loc -impl %{ml4-file} -o %{targets})))
-
-(rule
(targets g_prim.ml)
(deps (:mlg-file g_prim.mlg))
(action (run coqpp %{mlg-file})))