aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/mlutil.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/mlutil.ml')
-rw-r--r--plugins/extraction/mlutil.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index dba77b923..7d95d2e17 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1304,9 +1304,9 @@ let inline_test r t =
not (is_fix t2) && ml_size t < 12 && is_not_strict t)
let con_of_string s =
- let null = Dir_path.empty in
- match Dir_path.repr (dirpath_of_string s) with
- | id :: d -> make_con (MPfile (Dir_path.make d)) null (Label.of_id id)
+ let null = DirPath.empty in
+ match DirPath.repr (dirpath_of_string s) with
+ | id :: d -> make_con (MPfile (DirPath.make d)) null (Label.of_id id)
| [] -> assert false
let manual_inline_set =