aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThéo Zimmermann2018-10-22 09:19:13 +0200
committerThéo Zimmermann2018-10-22 09:19:13 +0200
commite605b73c34b0d796ac69e1953d3f5cb6975dfc0d (patch)
treec1278fa20cb0254147b65b9a9bfb01759dfbc647
parentfd214f1ad31d88c76dd928b6c6b039eaefcb21db (diff)
parent32c1fc1ec2973a5b579f3e1f1ce6acf66488f24b (diff)
Merge PR #8784: [dune] Remove rule for cLexer.ml4 -> cLexer.ml
-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})))