aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/loadpath.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-10 16:40:47 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-10 16:40:47 +0100
commit956b7c4304582b1e9e3ca0bb34944bcbac18c0cc (patch)
treeb6c8bfaf58e1e4ad3397ff8136142001d433cdd9 /library/loadpath.mli
parenta340265c9f88df990649481c8ecbe8a513ac4756 (diff)
parent9360af713794cb9ecf3c5e7d686c6f486a65df7f (diff)
Merge branch 'v8.5'
Diffstat (limited to 'library/loadpath.mli')
-rw-r--r--library/loadpath.mli7
1 files changed, 1 insertions, 6 deletions
diff --git a/library/loadpath.mli b/library/loadpath.mli
index 62dc5d591..d4029303d 100644
--- a/library/loadpath.mli
+++ b/library/loadpath.mli
@@ -15,11 +15,6 @@ open Names
*)
-type path_type =
- | ImplicitPath (** Can be implicitly appended to a logical path. *)
- | ImplicitRootPath (** Can be implicitly appended to the suffix of a logical path. *)
- | RootPath (** Can only be a prefix of a logical path. *)
-
type t
(** Type of loadpath bindings. *)
@@ -35,7 +30,7 @@ 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 -> path_type -> DirPath.t -> unit
+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
loadpaths. *)