aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-30 08:10:42 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-30 08:10:42 +0200
commitba3ccf80a44f0e06ee6e622a30f99de6804d005e (patch)
treee070e15d3e6cb54ba97601d938711cad7df64299 /tools/coqdoc
parent0336d4d19d446315cb922149b8ee4e7885843be0 (diff)
parentb30a6b141fed01a62330051bfb92c19564c93215 (diff)
Merge PR#692: Fail on deprecated warning even for Ocaml > 4.02.3
Diffstat (limited to 'tools/coqdoc')
-rw-r--r--tools/coqdoc/alpha.ml10
-rw-r--r--tools/coqdoc/index.ml6
-rw-r--r--tools/coqdoc/output.ml10
3 files changed, 19 insertions, 7 deletions
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index 3d92c9356..6a6db9556 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -8,7 +8,11 @@
open Cdglobals
-let norm_char_latin1 c = match Char.uppercase c with
+[@@@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
| '\192'..'\198' -> 'A'
| '\199' -> 'C'
| '\200'..'\203' -> 'E'
@@ -19,12 +23,12 @@ let norm_char_latin1 c = match Char.uppercase c with
| '\221' -> 'Y'
| c -> c
-let norm_char_utf8 c = Char.uppercase c
+let norm_char_utf8 c = uppercase c
let norm_char c =
if !utf8 then norm_char_utf8 c else
if !latin1 then norm_char_latin1 c else
- Char.uppercase c
+ uppercase c
let norm_string = String.map (fun s -> norm_char s)
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 34108eff4..4d118b978 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -155,10 +155,14 @@ 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 String.lowercase ln else "library"
+ if ln <> "" then lowercase ln else "library"
| Module -> "module"
| Definition -> "definition"
| Inductive -> "inductive"
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index e06ef9d76..972390579 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -19,6 +19,10 @@ 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 *)
@@ -846,7 +850,7 @@ module Html = struct
if t = Library then
let ln = !lib_name in
if ln <> "" then
- "[" ^ String.lowercase ln ^ "]", m ^ ".html", t
+ "[" ^ lowercase ln ^ "]", m ^ ".html", t
else
"[library]", m ^ ".html", t
else
@@ -864,7 +868,7 @@ module Html = struct
(* Impression de la table d'index *)
let print_index_table_item i =
- printf "<tr>\n<td>%s Index</td>\n" (String.capitalize i.idx_name);
+ printf "<tr>\n<td>%s Index</td>\n" (capitalize i.idx_name);
List.iter
(fun (c,l) ->
if l <> [] then
@@ -912,7 +916,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" (String.capitalize i.idx_name);
+ printf "<hr/>\n<h1>%s Index</h1>\n" (capitalize i.idx_name);
all_letters i
end
in