1 files changed, 49 insertions, 0 deletions
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.