- Synchronized subst_object with load_object (load_and_subst_objects)

  and set Declare ML Module as a regular substitutive object so that
  Declare ML Module is treated at the right place in the order of 
  appearance of substitutive declarations of a required module.
- Note: The full load/import mechanism for modules is not so clear: 
  the Require part of a Require Import inside a module is set outside 
  the module at module closing but the Import part remains inside (why not
  to put the "special" objects in the module too?); 
  moreover the "substitute" and "keep" objects of a module are
  desynchronised at module closing (is that really harmless/necessary?).
- Treatment of .cmxs targets in coq_makefile and in coqdep.
- Better make clean in coq_makefile generated makefiles.



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

2 files changed, 18 insertions, 8 deletions

diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index e2ea8250dd..fa5ded938d 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -90,7 +90,7 @@ let is_genrule r =
 
 let standard sds sps =
   print "Makefile.config:\n";
-  print "\t$(COQBIN)/coqtop -config > $@\n\n";
+  print "\t$(COQBIN)coqtop -config > $@\n\n";
   print "byte:\n";
   print "\t$(MAKE) all \"OPT:=-byte\"\n\n";
   print "opt:\n";
@@ -115,7 +115,7 @@ let standard sds sps =
     print "\n";
   end;
   print "clean:\n";
-  print "\trm -f *.cmo *.cmi *.cmx *.o $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~\n";
+  print "\trm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~\n";
   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) Makefile.config\n";
   if !some_mlfile then
@@ -147,12 +147,13 @@ 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) $(PP) $<\n\n";
-    print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\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: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
     print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
     print "%.ml.d: %.ml\n";
-    print "\t$(CAMLBIN)ocamldep -slash $(ZFLAGS) $(PP) \"$<\" > \"$@\"\n\n"
+    print "\t$(CAMLBIN)ocamldep -slash $(ZFLAGS) $(PP) -impl \"$<\" > \"$@\"\n\n"
   and v_rule () =
     print "%.vo %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
     print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n";
@@ -187,8 +188,8 @@ let variables l =
     print "GALLINA:=$(COQBIN)gallina\n";
     print "COQDOC:=$(COQBIN)coqdoc\n";
     (* Caml executables and relative variables *)
-    printf "CAMLC:=$(CAMLBIN)%s -rectypes -c\n" best_ocamlc;
-    printf "CAMLOPTC:=$(CAMLBIN)%s -rectypes -c\n" best_ocamlopt;
+    printf "CAMLC:=$(CAMLBIN)%s -rectypes\n" best_ocamlc;
+    printf "CAMLOPTC:=$(CAMLBIN)%s -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";
@@ -345,10 +346,15 @@ let all_target l =
       begin
 	print "MLFILES:="; print_list "\\\n  " mlfiles; print "\n";
 	print "CMOFILES:=$(MLFILES:.ml=.cmo)\n";
+	print "CMIFILES:=$(MLFILES:.ml=.cmi)\n";
+	print "CMXFILES:=$(MLFILES:.ml=.cmx)\n";
+	print "CMXSFILES:=$(MLFILES:.ml=.cmxs)\n";
+	print "OFILES:=$(MLFILES:.ml=.o)\n";
       end;
     print "\nall: ";
     if !some_vfile then print "$(VOFILES) ";
     if !some_mlfile then print "$(CMOFILES) ";
+    if Coq_config.has_natdynlink && !some_mlfile then print "$(CMXSFILES) ";
     print_list "\\\n  " other_targets; print "\n";
     if !some_vfile then 
       begin
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 5a31a64d8c..529ca0ba54 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -245,7 +245,11 @@ let traite_fichier_Coq verbose f =
 			addQueue deja_vu_ml s;
                	       try
               		 let mldir = Hashtbl.find mlKnown s in
-              		   printf " %s.cmo" (file_name ([String.uncapitalize s],mldir))
+			 let filename = file_name ([String.uncapitalize s],mldir) in
+              		 if Coq_config.has_natdynlink then
+			   printf " %s.cmo %s.cmxs" filename filename
+			 else
+			   printf " %s.cmo" filename
               	       with Not_found -> ()
 		     end)
 		sl