NEWCONTRIBVO doit apparaitre apres CONTRIBVO

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4531 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 83 insertions, 81 deletions

diff --git a/Makefile b/Makefile
index a0d53e190..54b2d45a5 100644
--- a/Makefile
+++ b/Makefile
@@ -676,81 +676,6 @@ sorting: $(SORTINGVO:%.vo=new%.vo)
 noreal: logic arith bool zarith lists sets intmap relations wellfounded \
 	setoids sorting
 
-NEWINITVO=$(INITVO:%.vo=new%.vo)
-NEWTHEORIESVO=$(THEORIESVO:%.vo=new%.vo)
-NEWCONTRIBVO=$(CONTRIBVO:%.vo=new%.vo)
-
-newinit:: $(NEWINITVO)
-newtheories:: $(NEWTHEORIESVO)
-newcontrib:: $(NEWCONTRIBVO) $(CONTRIBCMO)
-
-NEWINITV=$(INITVO:%.vo=new%.v)
-NEWTHEORIESV=$(THEORIESVO:%.vo=new%.v)
-NEWCONTRIBV=$(CONTRIBVO:%.vo=new%.v)
-
-translation:: $(NEWTHEORIESV) $(NEWCONTRIBV)
-
-###########################################################################
-# rules to make theories and states
-###########################################################################
-
-SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v
-
-states/barestate.coq: $(SYNTAXPP) $(BESTCOQTOP)
-	$(BESTCOQTOP) -v7 -boot -batch -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate $@
-
-states/initial.coq: states/barestate.coq states/MakeInitial.v $(INITVO) $(BESTCOQTOP)
-	$(BOOTCOQTOP) -v7 -batch -silent -is states/barestate.coq -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq
-
-states/initialnew.coq: states/MakeInitialNew.v $(NEWINITVO)
-	$(BOOTCOQTOP) -batch -silent -nois -load-vernac-source states/MakeInitialNew.v -outputstate states/initialnew.coq
-
-newtheories/Init/%.v: $(BESTCOQTOP) theories/Init/%.vo
-	@$(MKDIR) newtheories/Init
-	@cp -f theories/Init/$*.v8  newtheories/Init/$*.v
-
-theories/Init/%.vo: $(BESTCOQTOP) theories/Init/%.v
-	$(BOOTCOQTOP) -translate -no-strict -nois -compile theories/Init/$*
-
-newtheories/%.v: theories/%.vo
-	@$(MKDIR) newtheories/`dirname $*`
-	@cp -f theories/$*.v8  newtheories/$*.v
-
-theories/%.vo: theories/%.v states/initial.coq
-	$(BOOTCOQTOP) -translate -no-strict -compile theories/$*
-
-newcontrib/%.v: contrib/%.vo
-	@$(MKDIR) newcontrib/`dirname $*`
-	@cp -f contrib/$*.v8  newcontrib/$*.v
-
-contrib/%.vo: contrib/%.v states/initial.coq
-	$(BOOTCOQTOP) -translate -no-strict -compile contrib/$*
-
-newtheories/Init/%.vo: $(BESTCOQTOP) newtheories/Init/%.v
-	$(BOOTCOQTOP) -nois -compile $*
-
-newtheories/%.vo: newtheories/%.v states/initialnew.coq
-	$(BOOTCOQTOP) -compile newtheories/$*
-
-newcontrib/%.vo: newcontrib/%.v states/initialnew.coq
-	$(BOOTCOQTOP) -compile newcontrib/$*
-
-contrib/extraction/%.vo: contrib/extraction/%.v states/barestate.coq $(COQC)
-	$(BOOTCOQTOP) -translate -no-strict -is states/barestate.coq -compile $*
-clean::
-	rm -f states/*.coq
-
-# globalizations (for coqdoc)
-
-glob.dump::
-	rm -f glob.dump
-	rm -f theories/*/*.vo
-	$(MAKE) GLOB="-dump-glob glob.dump" world
-
-clean::
-	rm -f theories/*/*.vo
-
-
 ###########################################################################
 # contribs
 ###########################################################################
@@ -797,12 +722,6 @@ JPROVERVO=
 CCVO=\
  contrib/cc/CC.vo
 
-contrib/interface/Centaur.vo: contrib/interface/Centaur.v $(INTERFACE)
-	$(BESTCOQTOP) -translate -no-strict -boot -byte $(COQOPTS) -compile $*
-
-contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/initial.coq
-	$(BESTCOQTOP) -translate -no-strict -boot -byte  $(COQOPTS) -compile $*
-
 CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \
 	    $(CORRECTNESSVO) $(FOURIERVO) \
 	    $(JPROVERVO) $(INTERFACEVO) $(CCVO) $(FUNINDVO)
@@ -822,14 +741,97 @@ jprover: $(JPROVERVO) $(JPROVERCMO)
 funind: $(FUNINDCMO) $(FUNINDVO)
 cc: $(CCVO) $(CCCMO)
 
+NEWINITVO=$(INITVO:%.vo=new%.vo)
+NEWTHEORIESVO=$(THEORIESVO:%.vo=new%.vo)
+NEWCONTRIBVO=$(CONTRIBVO:%.vo=new%.vo)
+
+NEWINITV=$(INITVO:%.vo=new%.v)
+NEWTHEORIESV=$(THEORIESVO:%.vo=new%.v)
+NEWCONTRIBV=$(CONTRIBVO:%.vo=new%.v)
+
+# Made new*.v targets explicit, otherwise "make" removes them after use
+newinit:: $(NEWINITV) $(NEWINITVO)
+newtheories:: $(NEWTHEORIESV) $(NEWTHEORIESVO)
+newcontrib:: $(NEWCONTRIBV) $(NEWCONTRIBVO) $(CONTRIBCMO)
+
+translation:: $(NEWTHEORIESV) $(NEWCONTRIBV)
+
 ALLVO = $(INITVO) $(THEORIESVO) $(CONTRIBVO) $(EXTRACTIONVO)
 
+###########################################################################
+# rules to make theories, contrib and states
+###########################################################################
+
+SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v
+
+states/barestate.coq: $(SYNTAXPP) $(BESTCOQTOP)
+	$(BESTCOQTOP) -v7 -boot -batch -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate $@
+
+states/initial.coq: states/barestate.coq states/MakeInitial.v $(INITVO) $(BESTCOQTOP)
+	$(BOOTCOQTOP) -v7 -batch -silent -is states/barestate.coq -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq
+
+states/initialnew.coq: states/MakeInitialNew.v $(NEWINITVO)
+	$(BOOTCOQTOP) -batch -silent -nois -load-vernac-source states/MakeInitialNew.v -outputstate states/initialnew.coq
+
+newtheories/Init/%.v: $(BESTCOQTOP) theories/Init/%.vo
+	@$(MKDIR) newtheories/Init
+	@cp -f theories/Init/$*.v8  newtheories/Init/$*.v
+
+theories/Init/%.vo: $(BESTCOQTOP) theories/Init/%.v
+	$(BOOTCOQTOP) -translate -no-strict -nois -compile theories/Init/$*
+
+newtheories/%.v: theories/%.vo
+	@$(MKDIR) newtheories/`dirname $*`
+	@cp -f theories/$*.v8  newtheories/$*.v
+
+theories/%.vo: theories/%.v states/initial.coq
+	$(BOOTCOQTOP) -translate -no-strict -compile theories/$*
+
+newcontrib/%.v: contrib/%.vo
+	@$(MKDIR) newcontrib/`dirname $*`
+	@cp -f contrib/$*.v8  newcontrib/$*.v
+
+contrib/%.vo: contrib/%.v states/initial.coq
+	$(BOOTCOQTOP) -translate -no-strict -compile contrib/$*
+
+newtheories/Init/%.vo: $(BESTCOQTOP) newtheories/Init/%.v
+	$(BOOTCOQTOP) -nois -compile $*
+
+newtheories/%.vo: newtheories/%.v states/initialnew.coq
+	$(BOOTCOQTOP) -compile newtheories/$*
+
+newcontrib/%.vo: newcontrib/%.v states/initialnew.coq
+	$(BOOTCOQTOP) -compile newcontrib/$*
+
+contrib/extraction/%.vo: contrib/extraction/%.v states/barestate.coq $(COQC)
+	$(BOOTCOQTOP) -translate -no-strict -is states/barestate.coq -compile $*
+# Obsolete ?
+contrib/interface/Centaur.vo: contrib/interface/Centaur.v $(INTERFACE)
+	$(BESTCOQTOP) -translate -no-strict -boot -byte $(COQOPTS) -compile $*
+
+# Obsolete ?
+contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/initial.coq
+	$(BESTCOQTOP) -translate -no-strict -boot -byte  $(COQOPTS) -compile $*
+
+clean::
+	rm -f states/*.coq
+
+clean::
+	rm -f theories/*/*.vo
+
 clean::
 	rm -f contrib/*/*.cm[io] contrib/*/*.vo user-contrib/*.cm[io]
 
 archclean::
 	rm -f contrib/*/*.cmx contrib/*/*.[so]
 
+# globalizations (for coqdoc)
+
+glob.dump::
+	rm -f glob.dump
+	rm -f theories/*/*.vo
+	$(MAKE) GLOB="-dump-glob glob.dump" world
+
 ###########################################################################
 # tools
 ###########################################################################