- 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

1 files changed, 7 insertions, 0 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 553d353d6..7135a93cc 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -48,6 +48,13 @@ let subst_objects prefix subst seg =
   in
     list_smartmap subst_one seg
 
+let load_and_subst_objects i prefix subst seg =
+  List.rev (List.fold_left (fun seg (id,obj as node) ->
+    let obj' =  subst_object (make_oname prefix id, subst, obj) in
+    let node = if obj == obj' then node else (id, obj') in
+    load_object i (make_oname prefix id, obj');
+    node :: seg) [] seg)
+
 let classify_segment seg =
   let rec clean ((substl,keepl,anticipl) as acc) = function
     | (_,CompilingLibrary _) :: _ | [] -> acc