diff options
Diffstat (limited to 'tools/coqdoc/alpha.ml')
| -rw-r--r-- | tools/coqdoc/alpha.ml | 7 |
1 files changed, 1 insertions, 6 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 |