aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
diff options
context:
space:
mode:
authorGravatar Matej Kosik <matej.kosik@inria.fr>2017-03-23 14:42:24 +0100
committerGravatar Matej Kosik <matej.kosik@inria.fr>2017-06-01 10:24:10 +0200
commit466e6a97c97e83679d49f0867d8f571402e1548f (patch)
treed51d462b1713dd00d216bb5095d8545e15962e8f /Makefile.build
parentf3a388baf9cf2a14a658cab77554a0802b999486 (diff)
extract "plugins/micromega/micromega.ml{,i}" files from "plugins/micromega/MExtraction.v"
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build10
1 files changed, 10 insertions, 0 deletions
diff --git a/Makefile.build b/Makefile.build
index 8aedd9cec..32322cb0d 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -635,6 +635,16 @@ endif
$(SHOW)'COQDEP $<'
$(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET)
+# Below we provide those dependecies that are not discovered {coq,ocaml}dep programs.
+
+plugins/micromega/micromega.cmi \
+plugins/micromega/micromega.cmo \
+plugins/micromega/micromega.cmx \
+$(patsubst %.ml,%.ml.d,$(wildcard plugins/micromega/*.ml)) \
+$(patsubst %.mli,%.mli.d,$(wildcard plugins/micromega/*.mli)) \
+plugins/micromega/micromega_plugin.mlpack.d \
+ : plugins/micromega/MExtraction.vo
+
###########################################################################
# To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles