aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/coq_makefile.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 0e56cc3c0f..7bb1390cad 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -46,7 +46,7 @@ let usage_coq_makefile () =
\n\
\n[file.v]: Coq file to be compiled\
\n[file.ml[i4]?]: Objective Caml file to be compiled\
-\n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\
+\n[file.ml{lib,pack}]: ocamlbuild-style file that describes a Objective Caml\
\n library/module\
\n[any] : subdirectory that should be \"made\" and has a Makefile itself\
\n to do so. Very fragile and discouraged.\
@@ -248,7 +248,7 @@ let rec logic_gcd acc = function
let generate_conf_doc oc { defs; q_includes; r_includes } =
let includes = List.map (forget_source > snd) (q_includes @ r_includes) in
- let logpaths = List.map (CString.split '.') includes in
+ let logpaths = List.map (String.split_on_char '.') includes in
let gcd = logic_gcd [] logpaths in
let root =
if gcd = [] then
@@ -378,8 +378,8 @@ let destination_of { ml_includes; q_includes; r_includes; } file =
| _ -> assert false
let share_prefix s1 s2 =
- let s1 = CString.split '.' s1 in
- let s2 = CString.split '.' s2 in
+ let s1 = String.split_on_char '.' s1 in
+ let s2 = String.split_on_char '.' s2 in
match s1, s2 with
| x :: _ , y :: _ -> x = y
| _ -> false