diff options
| -rw-r--r-- | tools/coq_makefile.ml4 | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 82c6b72fa5..71fe04fa7d 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 |