Imported Upstream version 8.2~beta4.svn20080907+dfsgupstream/8.2.beta4.svn20080907+dfsg

1 files changed, 19 insertions, 11 deletions

diff --git a/Makefile.common b/Makefile.common
index 0a5d4260..a752892d 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -23,7 +23,7 @@ COQC:=bin/coqc$(EXE)
 COQTOPBYTE:=bin/coqtop.byte$(EXE)
 COQTOPOPT:=bin/coqtop.opt$(EXE)
 BESTCOQTOP:=bin/coqtop.$(BEST)$(EXE)
-COQTOP:=bin/coqtop$(EXE)
+COQTOPEXE:=bin/coqtop$(EXE)
 CHICKENBYTE:=bin/coqchk.byte$(EXE)
 CHICKENOPT:=bin/coqchk.opt$(EXE)
 BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE)
@@ -39,14 +39,14 @@ COQIDE:=bin/coqide$(EXE)
 
 ifeq ($(BEST),opt)
 COQBINARIES:= $(COQMKTOP) $(COQC) \
-  $(COQTOPBYTE) $(COQTOPOPT) $(COQTOP) $(CHICKENBYTE) $(CHICKENOPT) $(CHICKEN)
+  $(COQTOPBYTE) $(COQTOPOPT) $(COQTOPEXE) $(CHICKENBYTE) $(CHICKENOPT) $(CHICKEN)
 else
 COQBINARIES:= $(COQMKTOP) $(COQC) \
-  $(COQTOPBYTE)              $(COQTOP) $(CHICKENBYTE)               $(CHICKEN)
+  $(COQTOPBYTE)              $(COQTOPEXE) $(CHICKENBYTE)               $(CHICKEN)
 endif
 OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE)
 
-CSDPCERT:=bin/csdpcert$(EXE)
+CSDPCERT:=contrib/micromega/csdpcert$(EXE)
 
 ###########################################################################
 # tools
@@ -74,7 +74,7 @@ HEVEA:=hevea
 HEVEAOPTS:=-fix -exec xxdate.exe
 HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea
 export TEXINPUTS:=$(COQSRC)/doc:$(HEVEALIB):
-COQTEXOPTS:=-n 72 -image $(COQSRC)/$(COQTOP) -v -sl -small
+COQTEXOPTS:=-n 72 -image $(COQSRC)/$(COQTOPEXE) -v -sl -small
 
 DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex 
 
@@ -111,7 +111,9 @@ REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png)
 # Object and Source files 
 ###########################################################################
 
-LIBCOQRUN:=kernel/byterun/libcoqrun.a
+COQRUN := coqrun
+LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a
+DLLCOQRUN:=$(dir $(LIBCOQRUN))dll$(COQRUN).so
 
 CLIBS:=unix.cma
 
@@ -377,9 +379,9 @@ PARSERREQUIRES:=$(LINKCMO) $(LIBCOQRUN) # Solution de facilité...
 PARSERREQUIRESCMX:=$(LINKCMX)
 
 ifeq ($(BEST),opt)
-  COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE) bin/parser$(EXE) bin/parser.opt$(EXE)
+  COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE) bin/coq-parser$(EXE) bin/coq-parser.opt$(EXE)
 else
-  COQINTERFACE:=bin/coq-interface$(EXE) bin/parser$(EXE)
+  COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-parser$(EXE)
 endif
 
 PARSERCODE:=contrib/interface/line_parser.cmo contrib/interface/vtp.cmo \
@@ -811,6 +813,12 @@ CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
 ALLVO:= $(INITVO) $(THEORIESVO) $(CONTRIBVO)
 VFILES:= $(ALLVO:.vo=.v)
 
+# convert a (stdlib) filename into a module name:
+# remove .vo, replace theories and contrib by Coq, and replace slashes by dots
+vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst contrib/%,Coq.%,$(1:.vo=))))
+
+ALLMODS:=$(call vo_to_mod,$(ALLVO))
+
 LIBFILES:=$(THEORIESVO) $(CONTRIBVO)
 LIBFILESLIGHT:=$(THEORIESLIGHTVO)
 
@@ -821,10 +829,10 @@ INTERFACEVO:=
 
 MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
 	man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \
-	man/coqwc.1 man/coqdoc.1 \
+	man/coqwc.1 man/coqdoc.1 man/coqide.1 \
 	man/coq_makefile.1 man/coqmktop.1
 
-PCOQMANPAGES:=man/coq-interface.1 man/parser.1
+PCOQMANPAGES:=man/coq-interface.1 man/coq-parser.1
 
 RECTYPESML:=kernel/term.ml library/nametab.ml proofs/tacexpr.ml \
   parsing/pptactic.ml 
@@ -872,7 +880,7 @@ VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \
 DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq rectutorial refman-quick refman-nodep stdlib-nodep
 STAGE3_TARGETS:=world install coqide coqide-files coq coqlib \
   coqlight states pcoq-files check init theories theories-light contrib \
-  $(DOC_TARGETS) $(VO_TARGETS)
+  $(DOC_TARGETS) $(VO_TARGETS) validate
 
 
 # For emacs: