Merge PR #13275: Put all Int63 primitives in a separate file

Ack-by: SkySkimmer
Ack-by: ppedrot
Reviewed-by: vbgl

1 files changed, 11 insertions, 11 deletions

diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out
index eefa338f0d..ca8e1b58a8 100644
--- a/test-suite/output/Int63Syntax.out
+++ b/test-suite/output/Int63Syntax.out
@@ -1,7 +1,5 @@
 2%int63
      : int
-(2 + 2)%int63
-     : int
 2
      : int
 9223372036854775807
@@ -17,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.Int63.int
+Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int
 The command has indeed failed with message:
-Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.Int63.int
+Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int
 0
      : int
 0
@@ -32,13 +30,7 @@ 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
-2 + 2
-     : int
-     = 4
-     : int
-     = 37151199385380486
+add 2 2
      : int
 The command has indeed failed with message:
 int63 are only non-negative numbers.
@@ -56,3 +48,11 @@ t = 2%i63
      : nat
 2
      : int
+(2 + 2)%int63
+     : int
+2 + 2
+     : int
+     = 4
+     : int
+     = 37151199385380486
+     : int