Add a Char module.

4 files changed, 24 insertions, 0 deletions

diff --git a/_CoqProject b/_CoqProject
index 071066dd86..e2ef5cebe1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -35,6 +35,7 @@ src/ltac2_plugin.mlpack
 
 theories/Init.v
 theories/Int.v
+theories/Char.v
 theories/String.v
 theories/Ident.v
 theories/Array.v
diff --git a/src/tac2core.ml b/src/tac2core.ml
index ec10c335e9..b6983ed869 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -258,6 +258,16 @@ let () = define1 "int_neg" int begin fun m ->
   return (Value.of_int (~- m))
 end
 
+(** Char *)
+
+let () = define1 "char_of_int" int begin fun n ->
+  wrap (fun () -> Value.of_char (Char.chr n))
+end
+
+let () = define1 "char_to_int" char begin fun n ->
+  wrap (fun () -> Value.of_int (Char.code n))
+end
+
 (** String *)
 
 let () = define2 "string_make" int char begin fun n c ->
diff --git a/theories/Char.v b/theories/Char.v
new file mode 100644
index 0000000000..29fef60f2c
--- /dev/null
+++ b/theories/Char.v
@@ -0,0 +1,12 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Ltac2.Init.
+
+Ltac2 @external of_int : int -> char := "ltac2" "char_of_int".
+Ltac2 @external to_int : char -> int := "ltac2" "char_to_int".
diff --git a/theories/Ltac2.v b/theories/Ltac2.v
index 3fe71f4c65..e838fb7b81 100644
--- a/theories/Ltac2.v
+++ b/theories/Ltac2.v
@@ -9,6 +9,7 @@
 Require Export Ltac2.Init.
 
 Require Ltac2.Int.
+Require Ltac2.Char.
 Require Ltac2.String.
 Require Ltac2.Ident.
 Require Ltac2.Array.