Add hexadecimal numerals

We add hexadecimal numerals according to the following regexp
0[xX][0-9a-fA-F][0-9a-fA-F_]*(\.[0-9a-fA-F_]+)?([pP][+-]?[0-9][0-9_]*)?

This is unfortunately a rather large commit. I suggest reading it in
the following order:

* test-suite/output/ZSyntax.{v,out}       new test
* test-suite/output/Int63Syntax.{v,out}   ''
* test-suite/output/QArithSyntax.{v,out}  ''
* test-suite/output/RealSyntax.{v,out}    ''
* test-suite/output/FloatSyntax.{v,out}   ''

* interp/numTok.ml{i,}  extending numeral tokens

* theories/Init/Hexadecimal.v  adaptation of Decimal.v
                               for the new hexadecimal Numeral Notation
* theories/Init/Numeral.v  new interface for Numeral Notation (basically,
                           a numeral is either a decimal or an hexadecimal)

* theories/Init/Nat.v            add hexadecimal numeral notation to nat
* theories/PArith/BinPosDef.v    ''                                  positive
* theories/ZArith/BinIntDef.v    ''                                  Z
* theories/NArith/BinNatDef.v    ''                                  N
* theories/QArith/QArith_base.v  ''                                  Q

* interp/notation.ml{i,}     adapting implementation of numeral notations
* plugins/syntax/numeral.ml  ''

* plugins/syntax/r_syntax.ml  adapt parser for real numbers

* plugins/syntax/float_syntax.ml  adapt parser for primitive floats

* theories/Init/Prelude.v  register parser for nat
* adapting the test-suite (test-suite/output/NumeralNotations.{v,out}
  and test-suite/output/SearchPattern.out)
* remaining ml files (interp/constrex{tern,pr_ops}.ml where two open
  had to be permuted)

2 files changed, 32 insertions, 3 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 78b26c83ea..1729b9f85e 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1290,7 +1290,7 @@ Bind Scope Z_scope with Z.t Z.
 
 (** Re-export Notations *)
 
-Numeral Notation Z Z.of_int Z.to_int : Z_scope.
+Numeral Notation Z Z.of_num_int Z.to_num_int : Z_scope.
 
 Infix "+" := Z.add : Z_scope.
 Notation "- x" := (Z.opp x) : Z_scope.
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index c05ed9ebf4..8464ad1012 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -309,12 +309,32 @@ Definition to_pos (z:Z) : positive :=
 
 Definition of_uint (d:Decimal.uint) := of_N (Pos.of_uint d).
 
+Definition of_hex_uint (d:Hexadecimal.uint) := of_N (Pos.of_hex_uint d).
+
+Definition of_num_uint (d:Numeral.uint) :=
+  match d with
+  | Numeral.UIntDec d => of_uint d
+  | Numeral.UIntHex d => of_hex_uint d
+  end.
+
 Definition of_int (d:Decimal.int) :=
   match d with
   | Decimal.Pos d => of_uint d
   | Decimal.Neg d => opp (of_uint d)
   end.
 
+Definition of_hex_int (d:Hexadecimal.int) :=
+  match d with
+  | Hexadecimal.Pos d => of_hex_uint d
+  | Hexadecimal.Neg d => opp (of_hex_uint d)
+  end.
+
+Definition of_num_int (d:Numeral.int) :=
+  match d with
+  | Numeral.IntDec d => of_int d
+  | Numeral.IntHex d => of_hex_int d
+  end.
+
 Definition to_int n :=
   match n with
   | 0 => Decimal.Pos Decimal.zero
@@ -322,6 +342,15 @@ Definition to_int n :=
   | neg p => Decimal.Neg (Pos.to_uint p)
   end.
 
+Definition to_hex_int n :=
+  match n with
+  | 0 => Hexadecimal.Pos Hexadecimal.zero
+  | pos p => Hexadecimal.Pos (Pos.to_hex_uint p)
+  | neg p => Hexadecimal.Neg (Pos.to_hex_uint p)
+  end.
+
+Definition to_num_int n := Numeral.IntDec (to_int n).
+
 (** ** Iteration of a function
 
     By convention, iterating a negative number of times is identity.
@@ -639,9 +668,9 @@ Definition lxor a b :=
    | neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b))
  end.
 
-Numeral Notation Z of_int to_int : Z_scope.
+Numeral Notation Z of_num_int to_num_int : Z_scope.
 
 End Z.
 
 (** Re-export the notation for those who just [Import BinIntDef] *)
-Numeral Notation Z Z.of_int Z.to_int : Z_scope.
+Numeral Notation Z Z.of_num_int Z.to_num_int : Z_scope.