1 files changed, 57 insertions, 0 deletions
diff --git a/Makefile.vofiles b/Makefile.vofiles
new file mode 100644
index 0000000000..a71d68e565
--- /dev/null
+++ b/Makefile.vofiles
@@ -0,0 +1,57 @@
+
+# This file calls [find] and as such is not suitable for inclusion in
+# the test suite Makefile, unlike Makefile.common.
+
+ifdef QUICK
+VO=vio
+else
+VO=vo
+endif
+
+###########################################################################
+# vo files
+###########################################################################
+
+THEORIESVO := $(patsubst %.v,%.$(VO),$(shell find theories -type f -name "*.v"))
+PLUGINSVO := $(patsubst %.v,%.$(VO),$(shell find plugins -type f -name "*.v"))
+ALLVO := $(THEORIESVO) $(PLUGINSVO)
+VFILES := $(ALLVO:.$(VO)=.v)
+
+## More specific targets
+
+THEORIESLIGHTVO:= \
+ $(filter theories/Init/% theories/Logic/% theories/Unicode/% theories/Arith/%, $(THEORIESVO))
+
+# convert a (stdlib) filename into a module name:
+# remove .vo, replace theories and plugins by Coq, and replace slashes by dots
+vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=))))
+
+ALLMODS:=$(call vo_to_mod,$(ALLVO:.$(VO)=.vo))
+
+
+# Converting a stdlib filename into native compiler filenames
+# Used for install targets
+vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.cm*)))))
+
+vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.o)))))
+
+ifdef QUICK
+GLOBFILES:=
+else
+GLOBFILES:=$(ALLVO:.$(VO)=.glob)
+endif
+
+ifdef NATIVECOMPUTE
+NATIVEFILES := $(call vo_to_cm,$(ALLVO))
+ifeq ($(BEST),opt)
+NATIVEFILES += $(call vo_to_obj,$(ALLVO))
+endif
+else
+NATIVEFILES :=
+endif
+LIBFILES:=$(ALLVO:.$(VO)=.vo) $(NATIVEFILES) $(VFILES) $(GLOBFILES)
+
+# For emacs:
+# Local Variables:
+# mode: makefile-gmake
+# End: