diff options
| author | Pierre-Marie Pédrot | 2018-10-04 11:18:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-04 11:18:02 +0200 |
| commit | 8a5cb2d9da73b94e1713f5ee6cba73e0680f20fb (patch) | |
| tree | b66c100bb04261b43970d630b1cbf30b552fe90a /tools/coqdoc | |
| parent | 79da82da057224eec8abaf96c20b0725f18b2945 (diff) | |
| parent | 87d5e79baea4f3679a1429d2a2e128b564eec5d5 (diff) | |
Merge PR #8626: [ocaml] [lib] Remove some compatibility layers for OCaml < 4.03.0
Diffstat (limited to 'tools/coqdoc')
| -rw-r--r-- | tools/coqdoc/alpha.ml | 10 | ||||
| -rw-r--r-- | tools/coqdoc/index.ml | 6 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 11 |
3 files changed, 7 insertions, 20 deletions
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml index 269c1a1d50..36ce405fe6 100644 --- a/tools/coqdoc/alpha.ml +++ b/tools/coqdoc/alpha.ml @@ -10,11 +10,7 @@ open Cdglobals -[@@@ocaml.warning "-3"] (* Char.uppercase_ascii since 4.03.0 GPR#124 *) -let uppercase = Char.uppercase -[@@@ocaml.warning "+3"] - -let norm_char_latin1 c = match uppercase c with +let norm_char_latin1 c = match Char.uppercase_ascii c with | '\192'..'\198' -> 'A' | '\199' -> 'C' | '\200'..'\203' -> 'E' @@ -25,12 +21,12 @@ let norm_char_latin1 c = match uppercase c with | '\221' -> 'Y' | c -> c -let norm_char_utf8 c = uppercase c +let norm_char_utf8 c = Char.uppercase_ascii c let norm_char c = if !utf8 then norm_char_utf8 c else if !latin1 then norm_char_latin1 c else - uppercase c + Char.uppercase_ascii c let norm_string = String.map (fun s -> norm_char s) diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index 724d3838b0..8d395b418f 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -157,14 +157,10 @@ let sort_entries el = let display_letter c = if c = '*' then "other" else String.make 1 c -[@@@ocaml.warning "-3"] (* String.lowercase_ascii since 4.03.0 GPR#124 *) -let lowercase = String.lowercase -[@@@ocaml.warning "+3"] - let type_name = function | Library -> let ln = !lib_name in - if ln <> "" then lowercase ln else "library" + if ln <> "" then String.lowercase_ascii ln else "library" | Module -> "module" | Definition -> "definition" | Inductive -> "inductive" diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 05bc6aea9b..8ec8927abd 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -21,11 +21,6 @@ let printf s = Printf.fprintf !out_channel s let sprintf = Printf.sprintf -[@@@ocaml.warning "-3"] (* String.{capitalize,lowercase}_ascii since 4.03.0 GPR#124 *) -let capitalize = String.capitalize -let lowercase = String.lowercase -[@@@ocaml.warning "+3"] - (*s Coq keywords *) let build_table l = @@ -848,7 +843,7 @@ module Html = struct if t = Library then let ln = !lib_name in if ln <> "" then - "[" ^ lowercase ln ^ "]", m ^ ".html", t + "[" ^ String.lowercase_ascii ln ^ "]", m ^ ".html", t else "[library]", m ^ ".html", t else @@ -866,7 +861,7 @@ module Html = struct (* Impression de la table d'index *) let print_index_table_item i = - printf "<tr>\n<td>%s Index</td>\n" (capitalize i.idx_name); + printf "<tr>\n<td>%s Index</td>\n" (String.capitalize_ascii i.idx_name); List.iter (fun (c,l) -> if l <> [] then @@ -914,7 +909,7 @@ module Html = struct let print_table () = print_index_table all_index in let print_one_index i = if i.idx_size > 0 then begin - printf "<hr/>\n<h1>%s Index</h1>\n" (capitalize i.idx_name); + printf "<hr/>\n<h1>%s Index</h1>\n" (String.capitalize_ascii i.idx_name); all_letters i end in |
