Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 34 insertions, 40 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index d32a773d..d9fcdb24 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqinit.ml 11749 2009-01-05 14:01:04Z notin $ *)
+(* $Id$ *)
 
 open Pp
 open System
@@ -32,7 +32,7 @@ let load_rcfile() =
   if !load_rc then
     try
       if !rcfile_specified then
-        if file_readable_p !rcfile then 
+        if file_readable_p !rcfile then
           Vernac.load_vernac false !rcfile
         else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
       else if file_readable_p (!rcfile^"."^Coq_config.version) then
@@ -48,12 +48,9 @@ let load_rcfile() =
     with e ->
       (msgnl (str"Load of rcfile failed.");
        raise e)
-  else 
+  else
     Flags.if_verbose msgnl (str"Skipping rcfile loading.")
 
-let add_ml_include s =
-  Mltop.add_ml_dir s
-
 (* Puts dir in the path of ML and in the LoadPath *)
 let coq_add_path d s =
   Mltop.add_path d (Names.make_dirpath [Nameops.coq_root;Names.id_of_string s])
@@ -64,32 +61,29 @@ let includes = ref []
 let push_include (s, alias) = includes := (s,alias,false) :: !includes
 let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes
 
-(* Because find puts "./" and the loadpath is not nicely pretty-printed *)
-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/Unicode", "Unicode" ;
-    "theories/Classes", "Classes" ; 
-    "theories/Program", "Program" ; 
-    "theories/FSets", "FSets" ; 
-    "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/Numbers", "Numbers" ; 
-    "theories/QArith", "QArith" ; 
-    "theories/NArith", "NArith" ; 
-    "theories/ZArith", "ZArith" ; 
-    "theories/Arith", "Arith" ; 
-    "theories/Bool", "Bool" ; 
-    "theories/Logic", "Logic" ; 
+    "theories/Classes", "Classes" ;
+    "theories/Program", "Program" ;
+    "theories/MSets", "MSets" ;
+    "theories/FSets", "FSets" ;
+    "theories/Reals", "Reals" ;
+    "theories/Strings", "Strings" ;
+    "theories/Sorting", "Sorting" ;
+    "theories/Setoids", "Setoids" ;
+    "theories/Sets", "Sets" ;
+    "theories/Structures", "Structures" ;
+    "theories/Lists", "Lists" ;
+    "theories/Wellfounded", "Wellfounded" ;
+    "theories/Relations", "Relations" ;
+    "theories/Numbers", "Numbers" ;
+    "theories/QArith", "QArith" ;
+    "theories/NArith", "NArith" ;
+    "theories/ZArith", "ZArith" ;
+    "theories/Arith", "Arith" ;
+    "theories/Bool", "Bool" ;
+    "theories/Logic", "Logic" ;
     "theories/Init", "Init"
   ]
 
@@ -97,26 +91,26 @@ let theories_dirs_map = [
 let init_load_path () =
   let coqlib = Envars.coqlib () in
   let user_contrib = coqlib/"user-contrib" in
-  let dirs = "states" :: ["contrib"] in
+  let dirs = ["states";"plugins"] in
     (* first user-contrib *)
-    if Sys.file_exists user_contrib then 
+    if Sys.file_exists user_contrib then
       Mltop.add_rec_path user_contrib Nameops.default_root_prefix;
-    (* then states, contrib and dev *)
+    (* then states, theories and dev *)
     List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
     (* developer specific directory to open *)
     if Coq_config.local then coq_add_path (coqlib/"dev") "dev";
     (* 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])) 
+    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 current directory *)
     Mltop.add_path "." Nameops.default_root_prefix;
     (* additional loadpath, given with -I -include -R options *)
-    List.iter 
+    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 := []
 
@@ -124,11 +118,11 @@ let init_library_roots () =
    find the "include" file in the *source* directory *)
 let init_ocaml_path () =
   let coqsrc = Coq_config.coqsrc in
-  let add_subdir dl = 
-    Mltop.add_ml_dir (List.fold_left (/) coqsrc dl) 
+  let add_subdir dl =
+    Mltop.add_ml_dir (List.fold_left (/) coqsrc dl)
   in
-    Mltop.add_ml_dir (Envars.coqlib ()); 
+    Mltop.add_ml_dir (Envars.coqlib ());
     List.iter add_subdir
-      [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; 
+      [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ];
 	[ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
 	[ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ]