aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/mltop.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/mltop.mli')
-rw-r--r--toplevel/mltop.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index e368bf997..761a52d4a 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -43,8 +43,8 @@ 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.dir_path -> unit
-val add_rec_path : unix_path:string -> coq_root:Names.dir_path -> unit
+val add_path : unix_path:string -> coq_root:Names.Dir_path.t -> unit
+val add_rec_path : unix_path:string -> coq_root:Names.Dir_path.t -> unit
(** List of modules linked to the toplevel *)
val add_known_module : string -> unit