From d0243311634a8d6fa77fb2d0bb36eab96186a605 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Wed, 16 May 2018 20:36:34 +0200
Subject: Modify make system to include Makefile.common in the test suite

---
 Makefile.common | 36 ------------------------------------
 1 file changed, 36 deletions(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index f3b39ff26..9493acd1f 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -111,10 +111,6 @@ TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
 
 GRAMMARCMA:=grammar/grammar.cma
 
-# modules known by the toplevel of Coq
-
-OBJSMOD:=$(shell cat $(CORECMA:.cma=.mllib))
-
 ###########################################################################
 # plugins object files
 ###########################################################################
@@ -163,40 +159,8 @@ PLUGINSOPT:=$(PLUGINSCMO:.cmo=.cmxs)
 LINKCMO:=$(CORECMA) $(STATICPLUGINS)
 LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx)
 
-###########################################################################
-# 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))
-
 ALLSTDLIB := test-suite/misc/universes/all_stdlib
 
-# 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))
-
-
-# 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)))))
-
-GLOBFILES:=$(ALLVO:.vo=.glob)
-LIBFILES:=$(ALLVO) $(call vo_to_cm,$(ALLVO)) \
-	    $(call vo_to_obj,$(ALLVO)) \
-	    $(VFILES) $(GLOBFILES)
-
 # For emacs:
 # Local Variables:
 # mode: makefile
-- 
cgit v1.2.3