aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre Letouzey2014-01-24 17:12:32 +0100
committerPierre Letouzey2014-01-30 18:36:49 +0100
commit84b09aae2c727877c98e02508ddcd3b6a3ee9db7 (patch)
treeaef9f216795172206ea1131440f0295c5666e365
parent5db2b3e3b637d23befa6f97d78d8f411f436f4a5 (diff)
Mltop: explicitly qualify calls to CUnix
-rw-r--r--toplevel/mltop.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index ca325bc626..e0cb2209d5 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -10,7 +10,6 @@ open Errors
open Util
open Pp
open Flags
-open CUnix
open Libobject
open System
@@ -48,8 +47,9 @@ open System
(* This path is where we look for .cmo *)
let coq_mlpath_copy = ref ["."]
let keep_copy_mlpath path =
- let cpath = canonical_path_name path in
- let filter path' = not (String.equal cpath (canonical_path_name path')) in
+ let cpath = CUnix.canonical_path_name path in
+ let filter path' = not (String.equal cpath (CUnix.canonical_path_name path'))
+ in
coq_mlpath_copy := path :: List.filter filter !coq_mlpath_copy
(* If there is a toplevel under Coq *)