diff options
Diffstat (limited to 'test-suite/output/Int63Syntax.out')
| -rw-r--r-- | test-suite/output/Int63Syntax.out | 22 |
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 |