aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/common.ml9
-rw-r--r--plugins/extraction/haskell.ml6
-rw-r--r--plugins/extraction/table.ml9
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--plugins/funind/glob_termops.ml6
-rw-r--r--plugins/funind/indfun.ml2
6 files changed, 7 insertions, 29 deletions
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/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index fd2d90e9cf..0c45de4dc4 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -590,7 +590,6 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
*)
build_entry_lc env funnames avoid (mkGApp(b,args))
| GRec _ -> user_err Pp.(str "Not handled GRec")
- | GProj _ -> user_err Pp.(str "Funind does not support primitive projections")
| GProd _ -> user_err Pp.(str "Cannot apply a type")
end (* end of the application treatement *)
@@ -696,7 +695,6 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
| GRec _ -> user_err Pp.(str "Not handled GRec")
| GCast(b,_) ->
build_entry_lc env funnames avoid b
- | GProj(_,_) -> user_err Pp.(str "Funind does not support primitive projections")
and build_entry_lc_from_case env funname make_discr
(el:tomatch_tuples)
(brl:Glob_term.cases_clauses) avoid :
@@ -1246,7 +1244,7 @@ let rec compute_cst_params relnames params gt = DAst.with_val (function
discrimination ones *)
| GSort _ -> params
| GHole _ -> params
- | GIf _ | GRec _ | GCast _ | GProj _ ->
+ | GIf _ | GRec _ | GCast _ ->
raise (UserError(Some "compute_cst_params", str "Not handled case"))
) gt
and compute_cst_params_from_app acc (params,rtl) =
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 954fc3bab4..f81de82d5e 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -109,7 +109,6 @@ let change_vars =
| GCast(b,c) ->
GCast(change_vars mapping b,
Glob_ops.map_cast_type (change_vars mapping) c)
- | GProj(p,c) -> GProj(p, change_vars mapping c)
) rt
and change_vars_br mapping ({CAst.loc;v=(idl,patl,res)} as br) =
let new_mapping = List.fold_right Id.Map.remove idl mapping in
@@ -294,7 +293,6 @@ let rec alpha_rt excluded rt =
GApp(alpha_rt excluded f,
List.map (alpha_rt excluded) args
)
- | GProj(p,c) -> GProj(p, alpha_rt excluded c)
in
new_rt
@@ -346,7 +344,6 @@ let is_free_in id =
| GHole _ -> false
| GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
| GCast (b,CastCoerce) -> is_free_in b
- | GProj (_,c) -> is_free_in c
) x
and is_free_in_br {CAst.v=(ids,_,rt)} =
(not (Id.List.mem id ids)) && is_free_in rt
@@ -440,8 +437,6 @@ let replace_var_by_term x_id term =
| GCast(b,c) ->
GCast(replace_var_by_pattern b,
Glob_ops.map_cast_type replace_var_by_pattern c)
- | GProj(p,c) ->
- GProj(p,replace_var_by_pattern c)
) x
and replace_var_by_pattern_br ({CAst.loc;v=(idl,patl,res)} as br) =
if List.exists (fun id -> Id.compare id x_id == 0) idl
@@ -545,7 +540,6 @@ let expand_as =
| GCases(sty,po,el,brl) ->
GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
List.map (expand_as_br map) brl)
- | GProj(p,c) -> GProj(p, expand_as map c)
)
and expand_as_br map {CAst.loc; v=(idl,cpl,rt)} =
CAst.make ?loc (idl,cpl, expand_as (List.fold_left add_as map cpl) rt)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index e114a0119e..9eda19a86b 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -222,7 +222,6 @@ let is_rec names =
| GCases(_,_,el,brl) ->
List.exists (fun (e,_) -> lookup names e) el ||
List.exists (lookup_br names) brl
- | GProj(_,c) -> lookup names c
and lookup_br names {CAst.v=(idl,_,rt)} =
let new_names = List.fold_right Id.Set.remove idl names in
lookup new_names rt
@@ -783,7 +782,6 @@ let rec add_args id new_args = CAst.map (function
| CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.")
| CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.")
| CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.")
- | CProj _ -> user_err Pp.(str "Funind does not support primitive projections")
)
exception Stop of Constrexpr.constr_expr
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 18:12:55 +0000