diff options
| -rw-r--r-- | toplevel/coqinit.ml | 23 | ||||
| -rw-r--r-- | toplevel/coqinit.mli | 4 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 12 | ||||
| -rw-r--r-- | toplevel/mltop.ml | 9 | ||||
| -rw-r--r-- | toplevel/mltop.mli | 1 |
5 files changed, 17 insertions, 32 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 5222d87749..db77877efd 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -59,15 +59,12 @@ let load_rcfile() = (* Puts dir in the path of ML and in the LoadPath *) let coq_add_path unix_path s = - Mltop.add_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root;Names.Id.of_string s]) ~implicit:true; + Mltop.add_rec_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root;Names.Id.of_string s]) ~implicit:true; Mltop.add_ml_dir unix_path (* Recursively puts dir in the LoadPath if -nois was not passed *) let add_stdlib_path ~unix_path ~coq_root ~with_ml = - if !Flags.load_init then - Mltop.add_rec_path ~unix_path ~coq_root ~implicit:true - else - Mltop.add_path ~unix_path ~coq_root ~implicit:false; + Mltop.add_rec_path ~unix_path ~coq_root ~implicit:(!Flags.load_init); if with_ml then Mltop.add_rec_ml_dir unix_path @@ -77,8 +74,8 @@ let add_userlib_path ~unix_path = (* Options -I, -I-as, and -R of the command line *) let includes = ref [] -let push_include s alias recursive implicit = - includes := (s,alias,recursive,implicit) :: !includes +let push_include s alias implicit = + includes := (s, alias, implicit) :: !includes let ml_includes = ref [] let push_ml_include s = ml_includes := s :: !ml_includes @@ -109,13 +106,13 @@ let init_load_path () = List.iter (fun s -> add_userlib_path ~unix_path:s) xdg_dirs; (* then directories in COQPATH *) List.iter (fun s -> add_userlib_path ~unix_path:s) coqpath; - (* then current directory *) - Mltop.add_path ~unix_path:"." ~coq_root:Nameops.default_root_prefix ~implicit:false; - (* additional loadpath, given with options -I-as, -Q, and -R *) + (* then current directory (not recursively!) *) + Mltop.add_ml_dir "."; + Loadpath.add_load_path "." Nameops.default_root_prefix ~implicit:false; + (* additional loadpath, given with options -Q and -R *) List.iter - (fun (unix_path, coq_root, reci, implicit) -> - (if reci then Mltop.add_rec_path else Mltop.add_path) - ~unix_path ~coq_root ~implicit) + (fun (unix_path, coq_root, implicit) -> + Mltop.add_rec_path ~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/coqinit.mli b/toplevel/coqinit.mli index 5f7133c37c..c019cc1ced 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -15,8 +15,8 @@ val set_rcfile : string -> unit val no_load_rc : unit -> unit val load_rcfile : unit -> unit -val push_include : string -> Names.DirPath.t -> bool -> bool -> unit -(** [push_include phys_path log_path recursive implicit] *) +val push_include : string -> Names.DirPath.t -> bool -> unit +(** [push_include phys_path log_path implicit] *) val push_ml_include : string -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 5795de8857..e9e86953b3 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -135,9 +135,9 @@ let set_outputstate s = outputstate:=s let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate -let set_include d p recursive implicit = +let set_include d p implicit = let p = dirpath_of_string p in - push_include d p recursive implicit + push_include d p implicit let load_vernacular_list = ref ([] : (string * bool) list) let add_load_vernacular verb s = @@ -402,14 +402,12 @@ let parse_args arglist = (* Complex options with many args *) |"-I"|"-include" -> begin match rem with - | d :: "-as" :: p :: rem -> set_include d p false true; args := rem - | d :: "-as" :: [] -> error_missing_arg "-as" | d :: rem -> push_ml_include d; args := rem | [] -> error_missing_arg opt end |"-Q" -> begin match rem with - | d :: p :: rem -> set_include d p true false; args := rem + | d :: p :: rem -> set_include d p false; args := rem | _ -> error_missing_arg opt end |"-R" -> @@ -417,8 +415,8 @@ let parse_args arglist = | d :: "-as" :: [] -> error_missing_arg opt | d :: "-as" :: p :: rem -> warning "option -R * -as * deprecated, remove the -as"; - set_include d p true true; args := rem - | d :: p :: rem -> set_include d p true true; args := rem + set_include d p true; args := rem + | d :: p :: rem -> set_include d p true; args := rem | _ -> error_missing_arg opt end diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index ab3636956c..0b6fc48c47 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -161,15 +161,6 @@ let add_rec_ml_dir unix_path = (* Adding files to Coq and ML loadpath *) -let add_path ~unix_path:dir ~coq_root:coq_dirpath ~implicit = - if exists_dir dir then - begin - add_ml_dir dir; - Loadpath.add_load_path dir ~implicit coq_dirpath - end - else - msg_warning (str ("Cannot open " ^ dir)) - let convert_string d = try Names.Id.of_string d with UserError _ -> diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index 2a91afd88e..4f3f4ddde4 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -47,7 +47,6 @@ val add_ml_dir : string -> unit val add_rec_ml_dir : string -> unit (** Adds a path to the Coq and ML paths *) -val add_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit val add_rec_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit (** List of modules linked to the toplevel *) |