8 files changed, 145 insertions, 17 deletions
diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out
index 7ca4de1e46..96af456891 100644
--- a/test-suite/output/Int63Syntax.out
+++ b/test-suite/output/Int63Syntax.out
@@ -15,9 +15,9 @@
 427
      : int
 The command has indeed failed with message:
-Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int
+Cannot interpret this number as a value of type int
 The command has indeed failed with message:
-Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int
+Cannot interpret this number as a value of type int
 0
      : int
 0
@@ -33,9 +33,11 @@ The reference x was not found in the current environment.
 add 2 2
      : int
 The command has indeed failed with message:
-int63 are only non-negative numbers.
+Cannot interpret this number as a value of type int
 The command has indeed failed with message:
 overflow in int63 literal: 9223372036854775808
+0x1
+     : int
 2
      : nat
 2%int63
diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v
index 50910264f2..be0ee701af 100644
--- a/test-suite/output/Int63Syntax.v
+++ b/test-suite/output/Int63Syntax.v
@@ -20,6 +20,11 @@ Fail Check 0x.
 Check (PrimInt63.add 2 2).
 Fail Check -1.
 Fail Check 9223372036854775808.
+
+Set Printing All.
+Check 1%int63.
+Unset Printing All.
+
 Open Scope nat_scope.
 Check 2. (* : nat *)
 Check 2%int63.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 3477a293e3..0b18981f4e 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -77,18 +77,18 @@ fun x : nat => [x]
      : nat -> nat
 ∀ x : nat, x = x
      : Prop
-File "stdin", line 184, characters 0-160:
+File "stdin", line 187, characters 0-160:
 Warning: Notation "∀ _ .. _ , _" was already defined with a different format
 in scope type_scope. [notation-incompatible-format,parsing]
 ∀x : nat,x = x
      : Prop
-File "stdin", line 197, characters 0-60:
+File "stdin", line 200, characters 0-60:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 201, characters 0-64:
+File "stdin", line 204, characters 0-64:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 206, characters 0-62:
+File "stdin", line 209, characters 0-62:
 Warning: Lonely notation "_ %%%% _" was already defined with a different
 format. [notation-incompatible-format,parsing]
 3  %%  4
@@ -97,10 +97,10 @@ format. [notation-incompatible-format,parsing]
      : nat
 3   %%   4
      : nat
-File "stdin", line 234, characters 0-61:
+File "stdin", line 237, characters 0-61:
 Warning: The format modifier is irrelevant for only parsing rules.
 [irrelevant-format-only-parsing,parsing]
-File "stdin", line 238, characters 0-63:
+File "stdin", line 241, characters 0-63:
 Warning: The only parsing modifier has no effect in Reserved Notation.
 [irrelevant-reserved-notation-only-parsing,parsing]
 fun x : nat => U (S x)
@@ -111,7 +111,7 @@ fun x : nat => V x
      : forall x : nat, nat * (?T -> ?T)
 where
 ?T : [x : nat  x0 : ?T |- Type] (x0 cannot be used)
-File "stdin", line 255, characters 0-30:
+File "stdin", line 258, characters 0-30:
 Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing]
 0 :=: 0
      : Prop
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index ebad12af88..a5ec92fe3c 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -103,7 +103,10 @@ Module NumberNotations.
     Delimit Scope test17_scope with test17.
     Local Set Primitive Projections.
     Record myint63 := of_int { to_int : int }.
-    Number Notation myint63 of_int to_int : test17_scope.
+    Definition parse x :=
+      match x with Pos x => Some (of_int x) | Neg _ => None end.
+    Definition print x := Pos (to_int x).
+    Number Notation myint63 parse print : test17_scope.
     Check let v := 0%test17 in v : myint63.
   End Test17.
 End NumberNotations.
diff --git a/test-suite/output/NumberNotations.out b/test-suite/output/NumberNotations.out
index 60682edec8..df9b39389c 100644
--- a/test-suite/output/NumberNotations.out
+++ b/test-suite/output/NumberNotations.out
@@ -260,28 +260,28 @@ The command has indeed failed with message:
 add is not a constructor of an inductive type.
 The command has indeed failed with message:
 Missing mapping for constructor Iempty.
-File "stdin", line 574, characters 56-61:
+File "stdin", line 577, characters 56-61:
 Warning: Type of I'sum seems incompatible with the type of sum.
 Expected type is: (I' -> I' -> I') instead of (I -> I' -> I').
 This might yield ill typed terms when using the notation.
 [via-type-mismatch,numbers]
-File "stdin", line 579, characters 32-33:
+File "stdin", line 582, characters 32-33:
 Warning: I was already mapped to Set, mapping it also to
 nat might yield ill typed terms when using the notation.
 [via-type-remapping,numbers]
-File "stdin", line 579, characters 37-42:
+File "stdin", line 582, characters 37-42:
 Warning: Type of Iunit seems incompatible with the type of O.
 Expected type is: I instead of I.
 This might yield ill typed terms when using the notation.
 [via-type-mismatch,numbers]
 The command has indeed failed with message:
 'via' and 'abstract' cannot be used together.
-File "stdin", line 659, characters 21-23:
+File "stdin", line 662, characters 21-23:
 Warning: Type of I1 seems incompatible with the type of Fin.F1.
 Expected type is: (nat -> I) instead of I.
 This might yield ill typed terms when using the notation.
 [via-type-mismatch,numbers]
-File "stdin", line 659, characters 35-37:
+File "stdin", line 662, characters 35-37:
 Warning: Type of IS seems incompatible with the type of Fin.FS.
 Expected type is: (nat -> I -> I) instead of (I -> I).
 This might yield ill typed terms when using the notation.
diff --git a/test-suite/output/NumberNotations.v b/test-suite/output/NumberNotations.v
index 718da13500..85400c2fd4 100644
--- a/test-suite/output/NumberNotations.v
+++ b/test-suite/output/NumberNotations.v
@@ -328,7 +328,10 @@ Module Test17.
   Delimit Scope test17_scope with test17.
   Local Set Primitive Projections.
   Record myint63 := of_int { to_int : int }.
-  Number Notation myint63 of_int to_int : test17_scope.
+  Definition parse x :=
+    match x with Pos x => Some (of_int x) | Neg _ => None end.
+  Definition print x := Pos (to_int x).
+  Number Notation myint63 parse print : test17_scope.
   Check let v := 0%test17 in v : myint63.
 End Test17.
 
diff --git a/test-suite/output/Sint63Syntax.out b/test-suite/output/Sint63Syntax.out
new file mode 100644
index 0000000000..db14658307
--- /dev/null
+++ b/test-suite/output/Sint63Syntax.out
@@ -0,0 +1,66 @@
+2%sint63
+     : int
+2
+     : int
+-3
+     : int
+4611686018427387903
+     : int
+-4611686018427387904
+     : int
+427
+     : int
+427
+     : int
+427
+     : int
+427
+     : int
+427
+     : int
+The command has indeed failed with message:
+Cannot interpret this number as a value of type int
+The command has indeed failed with message:
+Cannot interpret this number as a value of type int
+0
+     : int
+0
+     : int
+The command has indeed failed with message:
+The reference xg was not found in the current environment.
+The command has indeed failed with message:
+The reference xG was not found in the current environment.
+The command has indeed failed with message:
+The reference x1 was not found in the current environment.
+The command has indeed failed with message:
+The reference x was not found in the current environment.
+2 + 2
+     : int
+The command has indeed failed with message:
+Cannot interpret this number as a value of type int
+The command has indeed failed with message:
+Cannot interpret this number as a value of type int
+0x1%int63
+     : int
+0x7fffffffffffffff%int63
+     : int
+2
+     : nat
+2%sint63
+     : int
+t = 2%si63
+     : int
+t = 2%si63
+     : int
+2
+     : nat
+2
+     : int
+(2 + 2)%sint63
+     : int
+2 + 2
+     : int
+     = 4
+     : int
+     = 37151199385380486
+     : int
diff --git a/test-suite/output/Sint63Syntax.v b/test-suite/output/Sint63Syntax.v
new file mode 100644
index 0000000000..b9ed596537
--- /dev/null
+++ b/test-suite/output/Sint63Syntax.v
@@ -0,0 +1,49 @@
+Require Import Sint63.
+
+Check 2%sint63.
+Open Scope sint63_scope.
+Check 2.
+Check -3.
+Check 4611686018427387903.
+Check -4611686018427387904.
+Check 0x1ab.
+Check 0X1ab.
+Check 0x1Ab.
+Check 0x1aB.
+Check 0x1AB.
+Fail Check 0x1ap5.  (* exponents not implemented (yet?) *)
+Fail Check 0x1aP5.
+Check 0x0.
+Check 0x000.
+Fail Check 0xg.
+Fail Check 0xG.
+Fail Check 00x1.
+Fail Check 0x.
+Check (PrimInt63.add 2 2).
+Fail Check 4611686018427387904.
+Fail Check -4611686018427387905.
+
+Set Printing All.
+Check 1%sint63.
+Check (-1)%sint63.
+Unset Printing All.
+
+Open Scope nat_scope.
+Check 2. (* : nat *)
+Check 2%sint63.
+Delimit Scope sint63_scope with si63.
+Definition t := 2%sint63.
+Print t.
+Delimit Scope nat_scope with sint63.
+Print t.
+Check 2.
+Close Scope nat_scope.
+Check 2.
+Close Scope sint63_scope.
+Delimit Scope sint63_scope with sint63.
+
+Check (2 + 2)%sint63.
+Open Scope sint63_scope.
+Check (2+2).
+Eval vm_compute in 2+2.
+Eval vm_compute in 65675757 * 565675998.