aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--clib/cString.ml7
-rw-r--r--clib/cString.mli4
-rw-r--r--clib/hashcons.ml4
-rw-r--r--ide/preferences.ml6
-rw-r--r--ide/protocol/xml_lexer.mll5
-rw-r--r--parsing/pcoq.mli8
-rw-r--r--plugins/extraction/common.ml9
-rw-r--r--plugins/extraction/haskell.ml6
-rw-r--r--plugins/extraction/table.ml9
-rw-r--r--tools/coqdep_common.ml6
-rw-r--r--tools/coqdep_lexer.mll9
-rw-r--r--tools/coqdoc/alpha.ml10
-rw-r--r--tools/coqdoc/index.ml6
-rw-r--r--tools/coqdoc/output.ml11
-rw-r--r--tools/ocamllibdep.mll9
15 files changed, 24 insertions, 85 deletions
diff --git a/clib/cString.ml b/clib/cString.ml
index dd33562f16..b178cbbd2c 100644
--- a/clib/cString.ml
+++ b/clib/cString.ml
@@ -13,9 +13,6 @@ module type S = module type of String
module type ExtS =
sig
include S
- [@@@ocaml.warning "-3"] (* [@@noalloc] since 4.03.0 GPR#240 *)
- external equal : string -> string -> bool = "caml_string_equal" "noalloc"
- [@@@ocaml.warning "+3"]
val hash : string -> int
val is_empty : string -> bool
val explode : string -> string list
@@ -37,10 +34,6 @@ end
include String
-[@@@ocaml.warning "-3"] (* [@@noalloc] since 4.03.0 GPR#240 *)
-external equal : string -> string -> bool = "caml_string_equal" "noalloc"
-[@@@ocaml.warning "+3"]
-
let rec hash len s i accu =
if i = len then accu
else
diff --git a/clib/cString.mli b/clib/cString.mli
index 2000dfafb5..df25a3821a 100644
--- a/clib/cString.mli
+++ b/clib/cString.mli
@@ -16,10 +16,6 @@ sig
include S
(** We include the standard library *)
- [@@@ocaml.warning "-3"] (* [@@noalloc] since 4.03.0 GPR#240 *)
- external equal : string -> string -> bool = "caml_string_equal" "noalloc"
- [@@@ocaml.warning "+3"]
-
(** Equality on strings *)
val hash : string -> int
diff --git a/clib/hashcons.ml b/clib/hashcons.ml
index 39969ebf75..4e5d6212a0 100644
--- a/clib/hashcons.ml
+++ b/clib/hashcons.ml
@@ -131,9 +131,7 @@ module Hstring = Make(
type u = unit
let hashcons () s =(* incr accesstr;*) s
- [@@@ocaml.warning "-3"] (* [@@noalloc] since 4.03.0 GPR#240 *)
- external eq : string -> string -> bool = "caml_string_equal" "noalloc"
- [@@@ocaml.warning "+3"]
+ let eq = String.equal
(** Copy from CString *)
let rec hash len s i accu =
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 3f10af04c9..9f04ced1c3 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -688,10 +688,6 @@ let pmodifiers ?(all = false) name p = modifiers
name
(str_to_mod_list p#get)
-[@@@ocaml.warning "-3"] (* String.uppercase_ascii since 4.03.0 GPR#124 *)
-let uppercase = String.uppercase
-[@@@ocaml.warning "+3"]
-
let configure ?(apply=(fun () -> ())) () =
let cmd_coqtop =
string
@@ -1018,7 +1014,7 @@ let configure ?(apply=(fun () -> ())) () =
let k =
if Int.equal (CString.length k) 1 && Util.is_letter k.[0] then k
else "" in
- let k = uppercase k in
+ let k = String.uppercase_ascii k in
[q, k]
in
diff --git a/ide/protocol/xml_lexer.mll b/ide/protocol/xml_lexer.mll
index 4a52147e17..e8bf7e16ae 100644
--- a/ide/protocol/xml_lexer.mll
+++ b/ide/protocol/xml_lexer.mll
@@ -83,9 +83,6 @@ let error lexbuf e =
last_pos := lexeme_start lexbuf;
raise (Error e)
-[@@@ocaml.warning "-3"] (* String.lowercase_ascii since 4.03.0 GPR#124 *)
-let lowercase = String.lowercase
-[@@@ocaml.warning "+3"]
}
let newline = ['\n']
@@ -222,7 +219,7 @@ and entity = parse
{
let ident = lexeme lexbuf in
try
- Hashtbl.find idents (lowercase ident)
+ Hashtbl.find idents (String.lowercase_ascii ident)
with
Not_found -> "&" ^ ident
}
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index e12ccaa636..c21f8f0d9a 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -26,14 +26,10 @@ module Gram : sig
type 'a entry = 'a Entry.e
[@@ocaml.deprecated "Use [Pcoq.Entry.t]"]
- [@@@ocaml.warning "-3"]
-
- val entry_create : string -> 'a entry
+ val entry_create : string -> 'a Entry.e
[@@ocaml.deprecated "Use [Pcoq.Entry.create]"]
- val gram_extend : 'a entry -> 'a Extend.extend_statement -> unit
-
- [@@@ocaml.warning "+3"]
+ val gram_extend : 'a Entry.e -> 'a Extend.extend_statement -> unit
end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index f235bb8986..d413cd1e6d 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -112,17 +112,12 @@ let pseudo_qualify = qualify "__"
let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
-[@@@ocaml.warning "-3"] (* String.(un)capitalize_ascii since 4.03.0 GPR#124 *)
-let capitalize = String.capitalize
-let uncapitalize = String.uncapitalize
-[@@@ocaml.warning "+3"]
-
-let lowercase_id id = Id.of_string (uncapitalize (ascii_of_id id))
+let lowercase_id id = Id.of_string (String.uncapitalize_ascii (ascii_of_id id))
let uppercase_id id =
let s = ascii_of_id id in
assert (not (String.is_empty s));
if s.[0] == '_' then Id.of_string ("Coq_"^s)
- else Id.of_string (capitalize s)
+ else Id.of_string (String.capitalize_ascii s)
type kind = Term | Type | Cons | Mod
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index e6234c1452..97fe9f24d5 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -21,10 +21,8 @@ open Mlutil
open Common
(*s Haskell renaming issues. *)
-[@@@ocaml.warning "-3"] (* String.(un)capitalize_ascii since 4.03.0 GPR#124 *)
-let pr_lower_id id = str (String.uncapitalize (Id.to_string id))
-let pr_upper_id id = str (String.capitalize (Id.to_string id))
-[@@@ocaml.warning "+3"]
+let pr_lower_id id = str (String.uncapitalize_ascii (Id.to_string id))
+let pr_upper_id id = str (String.capitalize_ascii (Id.to_string id))
let keywords =
List.fold_right (fun s -> Id.Set.add (Id.of_string s))
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index e05e82af6f..6ee1770a4e 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -22,11 +22,6 @@ open Util
open Pp
open Miniml
-[@@@ocaml.warning "-3"] (* String.capitalize_ascii since 4.03.0 GPR#124 *)
-let capitalize = String.capitalize
-[@@@ocaml.warning "+3"]
-
-
(** Sets and maps for [global_reference] that use the "user" [kernel_name]
instead of the canonical one *)
@@ -61,7 +56,7 @@ let is_modfile = function
| _ -> false
let raw_string_of_modfile = function
- | MPfile f -> capitalize (Id.to_string (List.hd (DirPath.repr f)))
+ | MPfile f -> String.capitalize_ascii (Id.to_string (List.hd (DirPath.repr f)))
| _ -> assert false
let is_toplevel mp =
@@ -784,7 +779,7 @@ let file_of_modfile mp =
let add_blacklist_entries l =
blacklist_table :=
- List.fold_right (fun s -> Id.Set.add (Id.of_string (capitalize s)))
+ List.fold_right (fun s -> Id.Set.add (Id.of_string (String.capitalize_ascii s)))
l !blacklist_table
(* Registration of operations for rollback. *)
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 23b8bc112e..6a913ea894 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -41,10 +41,6 @@ let norec_dirs = ref StrSet.empty
let suffixe = ref ".vo"
-[@@@ocaml.warning "-3"] (* String.capitalize_ascii since 4.03.0 GPR#124 *)
-let capitalize = String.capitalize
-[@@@ocaml.warning "+3"]
-
type dir = string option
(** [get_extension f l] checks whether [f] has one of the extensions
@@ -473,7 +469,7 @@ let mL_dependencies () =
printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname (String.concat " " dep);
printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname;
printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname;
- let efullname_capital = capitalize (Filename.basename efullname) in
+ let efullname_capital = String.capitalize_ascii (Filename.basename efullname) in
List.iter (fun dep ->
printf "%s.cmx : FOR_PACK=-for-pack %s\n" dep efullname_capital)
dep;
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index ade5e5be6f..5533ab106d 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -52,9 +52,6 @@
let s = Lexing.lexeme lexbuf in
check_valid lexbuf (String.sub s 1 (String.length s - 1))
- [@@@ocaml.warning "-3"] (* String.uncapitalize_ascii since 4.03.0 GPR#124 *)
- let uncapitalize = String.uncapitalize
- [@@@ocaml.warning "+3"]
}
let space = [' ' '\t' '\n' '\r']
@@ -159,7 +156,7 @@ and caml_action = parse
| space +
{ caml_action lexbuf }
| "open" space* (caml_up_ident as id)
- { Use_module (uncapitalize id) }
+ { Use_module (String.uncapitalize_ascii id) }
| "module" space+ caml_up_ident
{ caml_action lexbuf }
| caml_low_ident { caml_action lexbuf }
@@ -326,12 +323,12 @@ and modules mllist = parse
and qual_id ml_module_name = parse
| '.' [^ '.' '(' '[']
- { Use_module (uncapitalize ml_module_name) }
+ { Use_module (String.uncapitalize_ascii ml_module_name) }
| eof { raise Fin_fichier }
| _ { caml_action lexbuf }
and mllib_list = parse
- | caml_up_ident { let s = uncapitalize (Lexing.lexeme lexbuf)
+ | caml_up_ident { let s = String.uncapitalize_ascii (Lexing.lexeme lexbuf)
in s :: mllib_list lexbuf }
| "*predef*" { mllib_list lexbuf }
| space+ { mllib_list lexbuf }
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
diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll
index 382c39d3f2..053a0435ce 100644
--- a/tools/ocamllibdep.mll
+++ b/tools/ocamllibdep.mll
@@ -14,11 +14,6 @@
let syntax_error lexbuf =
raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf))
- [@@@ocaml.warning "-3"] (* String.(un)capitalize_ascii since 4.03.0 GPR#124 *)
- let uncapitalize = String.uncapitalize
-
- let capitalize = String.capitalize
- [@@@ocaml.warning "+3"]
}
let space = [' ' '\t' '\n' '\r']
@@ -31,7 +26,7 @@ let caml_low_ident = lowercase identchar*
rule mllib_list = parse
| uppercase+ { let s = Lexing.lexeme lexbuf in
s :: mllib_list lexbuf }
- | caml_up_ident { let s = uncapitalize (Lexing.lexeme lexbuf)
+ | caml_up_ident { let s = String.uncapitalize_ascii (Lexing.lexeme lexbuf)
in s :: mllib_list lexbuf }
| "*predef*" { mllib_list lexbuf }
| space+ { mllib_list lexbuf }
@@ -204,7 +199,7 @@ let mlpack_dependencies () =
List.iter
(fun (name,dirname) ->
let fullname = file_name name dirname in
- let modname = capitalize name in
+ let modname = String.capitalize_ascii name in
let deps = traite_fichier_modules fullname ".mlpack" in
let sdeps = String.concat " " deps in
let efullname = escape fullname in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:30:02 +0000