Modification de l'initialisation des chemins de la librairie standard

pour imposer un ordre précis des répertoires (résout en partie le
problème entre Init.Wf et Program.Wf.)



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

2 files changed, 46 insertions, 17 deletions

diff --git a/configure b/configure
index ad2973d975..6d497e29ff 100755
--- a/configure
+++ b/configure
@@ -649,7 +649,7 @@ PRINTF=`which printf`
 
 # Subdirectories of theories/ added in coq_config.ml
 subdirs () {
-    (cd $1; find * -type d ! -name .svn -exec $PRINTF "\"%s\";\n" {} \; | grep -v extraction/test | grep -v correctness >> "$mlconfig_file")
+    (cd $1; find * \( -name .svn -prune \) -o \( -type d -exec $PRINTF "\"%s\";\n" {} \; \) | grep -v extraction/test | grep -v correctness >> "$mlconfig_file")
 }
 
 echo "let theories_dirs = [" >> "$mlconfig_file"
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 00cc8be14b..85c61d2d15 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -68,6 +68,30 @@ let hm2 s =
   let n = String.length s in
   if n > 1 && s.[0] = '.' && s.[1] = '/' then String.sub s 2 (n-2) else s
 
+(* The list of all theories in the standard library /!\ order does matter *)
+let theories_dirs_map = [
+    "theories/Program", "Program" ; 
+    "theories/FSets", "FSets" ; 
+    "theories/IntMap", "IntMap" ; 
+    "theories/Reals", "Reals" ; 
+    "theories/Strings", "Strings" ; 
+    "theories/Sorting", "Sorting" ; 
+    "theories/Setoids", "Setoids" ; 
+    "theories/Sets", "Sets" ; 
+    "theories/Lists", "Lists" ; 
+    "theories/Wellfounded", "Wellfounded" ; 
+    "theories/Relations", "Relations" ; 
+    "theories/Ints", "Ints" ; 
+    "theories/Numbers", "Numbers" ; 
+    "theories/QArith", "QArith" ; 
+    "theories/NArith", "NArith" ; 
+    "theories/ZArith", "ZArith" ; 
+    "theories/Arith", "Arith" ; 
+    "theories/Bool", "Bool" ; 
+    "theories/Logic", "Logic" ; 
+    "theories/Init", "Init"
+  ]
+
 (* Initializes the LoadPath according to COQLIB and Coq_config *)
 let init_load_path () =
   (* developper specific directories to open *)
@@ -76,24 +100,29 @@ let init_load_path () =
     (* variable COQLIB overrides the default library *)
     getenv_else "COQLIB"
       (if Coq_config.local || !Options.boot then Coq_config.coqtop
-       else Coq_config.coqlib) in
-  (* first user-contrib *)
+	else Coq_config.coqlib) in
   let user_contrib = coqlib/"user-contrib" in
-  if Sys.file_exists user_contrib then 
-    Mltop.add_rec_path user_contrib Nameops.default_root_prefix;
-  (* then standard library *)
-  let vdirs = [ "theories"; "contrib" ] in
-  let dirs = "states" :: dev @ vdirs in
-  List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
+  let dirs = "states" :: "contrib" :: dev in
   let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
-  add_ml_include camlp4;
-  (* then current directory *)
-  Mltop.add_path "." Nameops.default_root_prefix;
-  (* additional loadpath, given with -I -include -R options *)
-  List.iter 
-    (fun (s,alias,reci) ->
-       if reci then Mltop.add_rec_path s alias else Mltop.add_path s alias)
-    (List.rev !includes)
+    (* first user-contrib *)
+    if Sys.file_exists user_contrib then 
+      Mltop.add_rec_path user_contrib Nameops.default_root_prefix;
+    (* then states, contrib and dev *)
+    List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
+    (* then standard library *)
+    List.iter 
+      (fun (s,alias) -> Mltop.add_rec_path (coqlib/s) (Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root])) 
+      theories_dirs_map;
+    (* then camlp4lib *)
+    add_ml_include camlp4;
+    (* then current directory *)
+    Mltop.add_path "." Nameops.default_root_prefix;
+    (* additional loadpath, given with -I -include -R options *)
+    List.iter 
+      (fun (s,alias,reci) ->
+	if reci then Mltop.add_rec_path s alias else Mltop.add_path s alias)
+      (List.rev !includes)
+      
 let init_library_roots () =
   includes := []