modules et coqc

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

1 files changed, 24 insertions, 5 deletions

diff --git a/Makefile b/Makefile
index 36d3fea4b1..974feb8b45 100644
--- a/Makefile
+++ b/Makefile
@@ -39,6 +39,9 @@ DEPFLAGS=$(LOCALINCLUDES)
 CAMLP4EXTEND=camlp4o $(INCLUDES) pa_extend.cmo
 OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS)
 OCAMLOPT_P4O=$(OCAMLOPT) -pp camlp4o $(OPTFLAGS)
+CAMLP4IFDEF=camlp4o pa_ifdef.cmo -D$(OSTYPE)
+
+COQINCLUDES=
 
 ###########################################################################
 # Objects files 
@@ -117,8 +120,9 @@ CMX=$(CMO:.cmo=.cmx) $(ARITHSYNTAX:.cmo=.cmx)
 ###########################################################################
 
 COQMKTOP=scripts/coqmktop
+COQC=scripts/coqc
 
-world: $(COQMKTOP) coqtop.byte coqtop.opt states tools
+world: $(COQMKTOP) $(COQC) coqtop.byte coqtop.opt states tools
 
 coqtop.opt: $(COQMKTOP) $(CMX)
 	$(COQMKTOP) -opt -notactics $(OPTFLAGS) -o coqtop.opt
@@ -131,7 +135,8 @@ coqtop.byte: $(COQMKTOP) $(CMO) Makefile
 COQMKTOPCMO=$(CONFIG) scripts/tolink.cmo scripts/coqmktop.cmo 
 
 $(COQMKTOP): $(COQMKTOPCMO)
-	$(OCAMLC) $(BYTEFLAGS) -o $(COQMKTOP) -custom str.cma unix.cma $(COQMKTOPCMO) $(OSDEPLIBS) $(STRLIB)
+	$(OCAMLC) $(BYTEFLAGS) -o $(COQMKTOP) -custom str.cma unix.cma \
+          $(COQMKTOPCMO) $(OSDEPLIBS) $(STRLIB)
 
 scripts/tolink.ml: Makefile
 	echo "let lib = \""$(LIB)"\"" > $@
@@ -146,6 +151,17 @@ scripts/tolink.ml: Makefile
 
 beforedepend:: scripts/tolink.ml
 
+# coqc
+
+COQCCMO=$(CONFIG) toplevel/usage.cmo scripts/coqc.cmo
+
+$(COQC): $(COQCCMO)
+	$(OCAMLC) $(BYTEFLAGS) -o $(COQC) -custom unix.cma $(COQCCMO) \
+	  $(OSDEPLIBS)
+
+scripts/coqc.cmo: scripts/coqc.ml4
+	$(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4IFDEF) -impl" -impl $<
+
 # we provide targets for each subdirectories
 
 lib: $(LIB)
@@ -179,6 +195,8 @@ tools/coqdep: $(COQDEPCMX)
 	$(OCAMLOPT) $(OPTFLAGS) -o tools/coqdep unix.cmxa $(COQDEPCMX) \
           $(OSDEPLIBS)
 
+beforedepend:: tools/coqdep
+
 GALLINACMX=tools/gallina_lexer.cmx tools/gallina.cmx
 
 tools/gallina: $(GALLINACMX)
@@ -321,8 +339,6 @@ beforedepend:: parsing/pcoq.ml parsing/extend.ml
 
 # toplevel/mltop.ml4 (ifdef Byte)
 
-CAMLP4IFDEF=camlp4o pa_ifdef.cmo
-
 toplevel/mltop.cmo: toplevel/mltop.ml4
 	$(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4IFDEF) -DByte -impl" -impl $<
 toplevel/mltop.cmx: toplevel/mltop.ml4
@@ -332,7 +348,7 @@ toplevel/mltop.cmx: toplevel/mltop.ml4
 # Default rules
 ###########################################################################
 
-.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .ml4 .el .elc
+.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .ml4 .v .vo .el .elc
 
 .ml.cmo:
 	$(OCAMLC) $(BYTEFLAGS) -c $<
@@ -352,6 +368,9 @@ toplevel/mltop.cmx: toplevel/mltop.ml4
 .ml4.cmx:
 	$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4EXTEND) -impl" -c -impl $<
 
+.v.vo:
+	$(COQC) $(COQCINCLUDES) $<
+
 .el.elc:
 	echo "(setq load-path (cons \".\" load-path))" > $*.compile
 	echo "(byte-compile-file \"$<\")" >> $*.compile