Merge branch 'v8.6'

5 files changed, 31 insertions, 26 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 59ee95b315..7ff59c4711 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -59,13 +59,12 @@ let load_rcfile() =
 
 (* Recursively puts dir in the LoadPath if -nois was not passed *)
 let add_stdlib_path ~unix_path ~coq_root ~with_ml =
-  Mltop.add_rec_path ~unix_path ~coq_root ~implicit:(!Flags.load_init);
-  if with_ml then
-    Mltop.add_rec_ml_dir unix_path
+  let add_ml = if with_ml then Mltop.AddRecML else Mltop.AddNoML in
+  Mltop.add_rec_path add_ml ~unix_path ~coq_root ~implicit:(!Flags.load_init)
 
 let add_userlib_path ~unix_path =
-  Mltop.add_rec_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false;
-  Mltop.add_rec_ml_dir unix_path
+  Mltop.add_rec_path Mltop.AddRecML ~unix_path
+    ~coq_root:Nameops.default_root_prefix ~implicit:false
 
 (* Options -I, -I-as, and -R of the command line *)
 let includes = ref []
@@ -90,7 +89,8 @@ let init_load_path () =
       Mltop.add_ml_dir (coqlib/"stm");
       Mltop.add_ml_dir (coqlib/"ide")
     end;
-    Mltop.add_ml_dir (coqlib/"toploop");
+    if System.exists_dir (coqlib/"toploop") then
+      Mltop.add_ml_dir (coqlib/"toploop");
     (* then standard library *)
     add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false;
     (* then plugins *)
@@ -108,7 +108,7 @@ let init_load_path () =
     (* additional loadpath, given with options -Q and -R *)
     List.iter
       (fun (unix_path, coq_root, implicit) ->
-        Mltop.add_rec_path ~unix_path ~coq_root ~implicit)
+        Mltop.add_rec_path Mltop.AddTopML ~unix_path ~coq_root ~implicit)
       (List.rev !includes);
     (* additional ml directories, given with option -I *)
     List.iter Mltop.add_ml_dir (List.rev !ml_includes)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a56459f180..ee331e37c7 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -227,18 +227,16 @@ let compile_file (v,f) =
     Vernac.compile v f
 
 let compile_files () =
-  match !compile_list with
-    | [] -> ()
-    | [vf] -> compile_file vf (* One compilation : no need to save init state *)
-    | l ->
-      let init_state = States.freeze ~marshallable:`No in
-      let coqdoc_init_state = CLexer.location_table () in
-      List.iter
-        (fun vf ->
-	  States.unfreeze init_state;
-	  CLexer.restore_location_table coqdoc_init_state;
-          compile_file vf)
-        (List.rev l)
+  if !compile_list == [] then ()
+  else
+    let init_state = States.freeze ~marshallable:`No in
+    let coqdoc_init_state = CLexer.location_table () in
+    Feedback.(add_feeder debug_feeder);
+    List.iter (fun vf ->
+        States.unfreeze init_state;
+        CLexer.restore_location_table coqdoc_init_state;
+        compile_file vf)
+      (List.rev !compile_list)
 
 (** Options for proof general *)
 
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index f9e0bc34ac..6b62f7aeb8 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -45,12 +45,12 @@ open System
    to build a dummy dynlink.cmxa, cf. dev/dynlink.ml. *)
 
 (* This path is where we look for .cmo *)
-let coq_mlpath_copy = ref ["."]
+let coq_mlpath_copy = ref [Sys.getcwd ()]
 let keep_copy_mlpath path =
   let cpath = CUnix.canonical_path_name path in
-  let filter path' = not (String.equal cpath (CUnix.canonical_path_name path'))
+  let filter path' = not (String.equal cpath path')
   in
-  coq_mlpath_copy := path :: List.filter filter !coq_mlpath_copy
+  coq_mlpath_copy := cpath :: List.filter filter !coq_mlpath_copy
 
 (* If there is a toplevel under Coq *)
 type toplevel = {
@@ -182,7 +182,9 @@ let warn_cannot_open_path =
   CWarnings.create ~name:"cannot-open-path" ~category:"filesystem"
       (fun unix_path -> str "Cannot open " ++ str unix_path)
 
-let add_rec_path ~unix_path ~coq_root ~implicit =
+type add_ml = AddNoML | AddTopML | AddRecML
+
+let add_rec_path add_ml ~unix_path ~coq_root ~implicit =
   if exists_dir unix_path then
     let dirs = all_subdirs ~unix_path in
     let prefix = Names.DirPath.repr coq_root in
@@ -193,7 +195,10 @@ let add_rec_path ~unix_path ~coq_root ~implicit =
       with Exit -> None
     in
     let dirs = List.map_filter convert_dirs dirs in
-    let () = add_ml_dir unix_path in
+    let () = match add_ml with
+      | AddNoML -> ()
+      | AddTopML -> add_ml_dir unix_path
+      | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs in
     let add (path, dir) =
       Loadpath.add_load_path path ~implicit dir in
     let () = List.iter add dirs in
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 5d05468241..6633cb9372 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -46,8 +46,10 @@ val dir_ml_use : string -> unit
 val add_ml_dir : string -> unit
 val add_rec_ml_dir : string -> unit
 
+type add_ml = AddNoML | AddTopML | AddRecML
+
 (** Adds a path to the Coq and ML paths *)
-val add_rec_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit
+val add_rec_path : add_ml -> unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit
 
 (** List of modules linked to the toplevel *)
 val add_known_module : string -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6e632999c8..eebc9ff663 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -880,7 +880,7 @@ let expand filename =
 let vernac_add_loadpath implicit pdir ldiropt =
   let pdir = expand pdir in
   let alias = Option.default Nameops.default_root_prefix ldiropt in
-  Mltop.add_rec_path ~unix_path:pdir ~coq_root:alias ~implicit
+  Mltop.add_rec_path Mltop.AddTopML ~unix_path:pdir ~coq_root:alias ~implicit
 
 let vernac_remove_loadpath path =
   Loadpath.remove_load_path (expand path)