diff options
Diffstat (limited to 'test-suite/output/Int63Syntax.v')
| -rw-r--r-- | test-suite/output/Int63Syntax.v | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v index c49616d918..6f1046f7a5 100644 --- a/test-suite/output/Int63Syntax.v +++ b/test-suite/output/Int63Syntax.v @@ -1,7 +1,6 @@ -Require Import Int63 Cyclic63. +Require Import PrimInt63. Check 2%int63. -Check (2 + 2)%int63. Open Scope int63_scope. Check 2. Check 9223372036854775807. @@ -18,10 +17,7 @@ Fail Check 0xg. Fail Check 0xG. Fail Check 00x1. Fail Check 0x. -Check (Int63.add 2 2). -Check (2+2). -Eval vm_compute in 2+2. -Eval vm_compute in 65675757 * 565675998. +Check (PrimInt63.add 2 2). Fail Check -1. Fail Check 9223372036854775808. Open Scope nat_scope. @@ -36,3 +32,11 @@ Check 2. Close Scope nat_scope. Check 2. Close Scope int63_scope. + +Require Import Int63. + +Check (2 + 2)%int63. +Open Scope int63_scope. +Check (2+2). +Eval vm_compute in 2+2. +Eval vm_compute in 65675757 * 565675998. |