aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-02-23 13:48:47 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-14 22:19:27 +0100
commit92579449f62f0fd7699b0b447f3aee0d82d1b5c3 (patch)
treed4e92bb8b814467be59ee8a7de91bec4b3cabcec /tools/coqdoc
parentfacf0520a47603d2679508136cbed43def0744cc (diff)
[safe-string] tools
No functional changes.
Diffstat (limited to 'tools/coqdoc')
-rw-r--r--tools/coqdoc/alpha.ml7
-rw-r--r--tools/coqdoc/index.ml4
2 files changed, 3 insertions, 8 deletions
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index f817ed5a2..3d92c9356 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -26,12 +26,7 @@ let norm_char c =
if !latin1 then norm_char_latin1 c else
Char.uppercase c
-let norm_string s =
- let u = String.copy s in
- for i = 0 to String.length s - 1 do
- u.[i] <- norm_char s.[i]
- done;
- u
+let norm_string = String.map (fun s -> norm_char s)
let compare_char c1 c2 = match norm_char c1, norm_char c2 with
| ('A'..'Z' as c1), ('A'..'Z' as c2) -> compare c1 c2
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 9be791a8d..c9cb676e9 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -197,7 +197,7 @@ let prepare_entry s = function
let h = try String.index_from s 0 ':' with _ -> err () in
let i = try String.index_from s (h+1) ':' with _ -> err () in
let sc = String.sub s (h+1) (i-h-1) in
- let ntn = String.make (String.length s - i) ' ' in
+ let ntn = Bytes.make (String.length s - i) ' ' in
let k = ref 0 in
let j = ref (i+1) in
let quoted = ref false in
@@ -220,7 +220,7 @@ let prepare_entry s = function
end;
incr j
done;
- let ntn = String.sub ntn 0 !k in
+ let ntn = Bytes.sub_string ntn 0 !k in
if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")"
| _ ->
s