From 1a14905e4bdb62098f35ae5c0bb8fe710ec8ecb2 Mon Sep 17 00:00:00 2001 From: pboutill Date: Thu, 7 Jul 2011 15:17:02 +0000 Subject: coq_makefile bug fix 2405: cmxs are now made from cmx files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14271 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tools/coq_makefile.ml4 | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'tools/coq_makefile.ml4') diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 82c6b72fa..71fe04fa7 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -287,16 +287,16 @@ let implicit () = let ml4_rules () = 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$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $<\n\n"; print "%.ml4.d: %.ml4\n"; print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"in let ml_rules () = print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print "%.cmxs: %.ml\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n"; print "%.ml.d: %.ml\n"; - print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" - and v_rule () = + print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + let cmxs_rules () = + print "%.cmxs: %.cmx\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n" in + let v_rules () = print "%.vo %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n"; print "%.g: %.v\n\t$(GALLINA) $<\n\n"; @@ -310,7 +310,8 @@ let implicit () = if !some_mlifile then mli_rules (); if !some_ml4file then ml4_rules (); if !some_mlfile then ml_rules (); - if !some_vfile then v_rule () + if !some_mlfile || !some_ml4file then cmxs_rules (); + if !some_vfile then v_rules () let variables defs = let var_aux (v,def) = print v; print "="; print def; print "\n" in -- cgit v1.2.3