diff options
| -rw-r--r-- | library/loadpath.ml | 4 | ||||
| -rw-r--r-- | library/loadpath.mli | 8 | ||||
| -rw-r--r-- | toplevel/mltop.ml | 6 |
3 files changed, 8 insertions, 10 deletions
diff --git a/library/loadpath.ml b/library/loadpath.ml index 0f7c2fb46..ca2280102 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -17,7 +17,6 @@ open Libnames type t = { path_physical : CUnix.physical_path; path_logical : DirPath.t; - path_root : bool; path_implicit : bool; } @@ -53,13 +52,12 @@ let remove_load_path dir = let filter p = not (String.equal p.path_physical dir) in load_paths := List.filter filter !load_paths -let add_load_path phys_path coq_path ~root ~implicit = +let add_load_path phys_path coq_path ~implicit = let phys_path = CUnix.canonical_path_name phys_path in let filter p = String.equal p.path_physical phys_path in let binding = { path_logical = coq_path; path_physical = phys_path; - path_root = root; path_implicit = implicit; } in match List.filter filter !load_paths with diff --git a/library/loadpath.mli b/library/loadpath.mli index d4029303d..ae54b3183 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -30,8 +30,8 @@ val get_load_paths : unit -> t list val get_paths : unit -> CUnix.physical_path list (** Same as [get_load_paths] but only get the physical part. *) -val add_load_path : CUnix.physical_path -> DirPath.t -> root:bool -> implicit:bool -> unit -(** [add_load_path phys type log] adds the binding [phys := log] to the current +val add_load_path : CUnix.physical_path -> DirPath.t -> implicit:bool -> unit +(** [add_load_path phys log type] adds the binding [phys := log] to the current loadpaths. *) val remove_load_path : CUnix.physical_path -> unit @@ -47,7 +47,7 @@ val is_in_load_paths : CUnix.physical_path -> bool val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list (** Given a relative logical path, associate the list of absolute physical and - logical paths which are possible expansions of it. *) + logical paths which are possible matches of it. *) val expand_root_path : DirPath.t -> CUnix.physical_path list -(** As [expand_path] but restricts to root loadpaths. *) +(** As [expand_path] but ignores the implicit status. *) diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 357c5482f..ab3636956 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -165,7 +165,7 @@ 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 ~root:true ~implicit coq_dirpath + Loadpath.add_load_path dir ~implicit coq_dirpath end else msg_warning (str ("Cannot open " ^ dir)) @@ -189,9 +189,9 @@ let add_rec_path ~unix_path ~coq_root ~implicit = let dirs = List.map_filter convert_dirs dirs in let () = add_ml_dir unix_path in let add (path, dir) = - Loadpath.add_load_path path ~root:false ~implicit dir in + Loadpath.add_load_path path ~implicit dir in let () = List.iter add dirs in - Loadpath.add_load_path unix_path ~root:true ~implicit coq_root + Loadpath.add_load_path unix_path ~implicit coq_root else msg_warning (str ("Cannot open " ^ unix_path)) |