diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:35 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:35 +0200 |
| commit | e4282ea99c664d8d58067bee199cbbcf881b60d5 (patch) | |
| tree | d4c4a873eb055c728666f367469fa26c3417793a /tools/coq_makefile.ml4 | |
| parent | a0a94c1340a63cdb824507b973393882666ba52a (diff) | |
Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg
Diffstat (limited to 'tools/coq_makefile.ml4')
| -rw-r--r-- | tools/coq_makefile.ml4 | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 98457261..eb3a19fa 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq_makefile.ml4 11883 2009-02-06 09:54:52Z herbelin $ *) +(* $Id: coq_makefile.ml4 12176 2009-06-09 09:44:40Z notin $ *) (* créer un Makefile pour un développement Coq automatiquement *) @@ -212,7 +212,7 @@ let clean sds sps = print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) \ $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)\n"; if !some_mlfile then - print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d)\n"; + print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d) $(MLFILES:.ml=.cmx) $(MLFILES:.ml=.o)\n"; if Coq_config.has_natdynlink && !some_mlfile then print "\trm -f $(CMXSFILES) $(CMXSFILES:.cmxs=.o)\n"; print "\t- rm -rf html\n"; @@ -243,14 +243,14 @@ let footer_includes () = let implicit () = let ml_rules () = print "%.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) -c $(PP) $<\n\n"; - print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -c $(PP) $<\n\n"; - print "%.cmxs: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<\n\n"; + print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n"; + print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n"; + print "%.cmxs: %.ml\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<\n\n"; print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; - print "%.cmxs: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $<\n\n"; + print "%.cmxs: %.ml4\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $<\n\n"; print "%.ml.d: %.ml\n"; - print "\t$(CAMLBIN)ocamldep -slash $(COQSRCLIBS) $(PP) \"$<\" > \"$@\"\n\n" + print "\t$(CAMLBIN)ocamldep -slash $(COQSRCLIBS) $(OCAMLLIBS) $(PP) \"$<\" > \"$@\"\n\n" and v_rule () = print "%.vo %.glob: %.v\n\t$(COQC) -dump-glob $*.glob $(COQDEBUG) $(COQFLAGS) $*\n\n"; print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n"; @@ -283,8 +283,8 @@ let variables defs = print "COQDOC:=$(COQBIN)coqdoc\n"; print "COQMKTOP:=$(COQBIN)coqmktop\n"; (* Caml executables and relative variables *) - printf "CAMLC:=$(CAMLBIN)%s -rectypes\n" best_ocamlc; - printf "CAMLOPTC:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt; + printf "CAMLC:=$(CAMLBIN)%s -c -rectypes\n" best_ocamlc; + printf "CAMLOPTC:=$(CAMLBIN)%s -c -rectypes\n" best_ocamlopt; printf "CAMLLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlc; printf "CAMLOPTLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt; print "GRAMMARS:=grammar.cma\n"; @@ -315,7 +315,7 @@ let include_dirs (inc_i,inc_r) = let str_i' = parse_includes inc_i' in let str_r = parse_rec_includes inc_r in section "Libraries definitions."; - print "OCAMLLIBS:=-I $(CAMLP4LIB) "; print_list "\\\n " str_i; print "\n"; + print "OCAMLLIBS:="; print_list "\\\n " str_i; print "\n"; print "COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \\ -I $(COQLIB)/library -I $(COQLIB)/parsing \\ -I $(COQLIB)/pretyping -I $(COQLIB)/interp \\ |