Merge PR #18369: Ltac2.Char.of_int: use throw instead of raw except…

…ion for invalid argument

Reviewed-by: ppedrot
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

plugins/ltac2/tac2core.ml

@@ -438,7 +438,12 @@ let () = define "int_lnot" (int @-> ret int) lnot
 
 (** Char *)
 
-let () = define "char_of_int" (int @-> ret char) Char.chr
+let () = define "char_of_int" (int @-> tac char) @@ fun i ->
+  try return (Char.chr i)
+  with Invalid_argument _ as e ->
+    let e, info = Exninfo.capture e in
+    throw ~info e
+
 let () = define "char_to_int" (char @-> ret int) Char.code
 
 (** String *)

user-contrib/Ltac2/Char.v

@@ -12,6 +12,8 @@ Require Import Ltac2.Init.
 Require Ltac2.Int.
 
 Ltac2 @external of_int : int -> char := "coq-core.plugins.ltac2" "char_of_int".
+(** Throws if the integer is not a valid char (in range [0-255]). *)
+
 Ltac2 @external to_int : char -> int := "coq-core.plugins.ltac2" "char_to_int".
 
 Ltac2 equal (x : char) (y : char) : bool := Int.equal (to_int x) (to_int y).