Signed primitive integers

Signed primitive integers defined on top of the existing unsigned ones
with two's complement.

The module Sint63 includes the theory of signed primitive integers that
differs from the unsigned case.

Additions to the kernel:
  les (signed <=), lts (signed <), compares (signed compare),
  divs (signed division), rems (signed remainder),
  asr (arithmetic shift right)
(The s suffix is not used when importing the Sint63 module.)

The printing and parsing of primitive ints was updated and the
int63_syntax_plugin was removed (we use Number Notation instead).

A primitive int is parsed / printed as unsigned or signed depending on
the scope. In the default (Set Printing All) case, it is printed in
hexadecimal.

13 files changed, 462 insertions, 0 deletions

diff --git a/test-suite/primitive/sint63/add.v b/test-suite/primitive/sint63/add.v
new file mode 100644
index 0000000000..dcafd64181
--- /dev/null
+++ b/test-suite/primitive/sint63/add.v
@@ -0,0 +1,25 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 2 + 3 = 5).
+Check (eq_refl 5 <: 2 + 3 = 5).
+Check (eq_refl 5 <<: 2 + 3 = 5).
+Definition compute1 := Eval compute in 2 + 3.
+Check (eq_refl compute1 : 5 = 5).
+
+Check (eq_refl : 4611686018427387903 + 1 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <:
+  4611686018427387903 + 1 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <<:
+  4611686018427387903 + 1 = -4611686018427387904).
+Definition compute2 := Eval compute in 4611686018427387903 + 1.
+Check (eq_refl compute2 : -4611686018427387904 = -4611686018427387904).
+
+Check (eq_refl : 2 - 3 = -1).
+Check (eq_refl (-1) <: 2 - 3 = -1).
+Check (eq_refl (-1) <<: 2 - 3 = -1).
+Definition compute3 := Eval compute in 2 - 3.
+Check (eq_refl compute3 : -1 = -1).
diff --git a/test-suite/primitive/sint63/asr.v b/test-suite/primitive/sint63/asr.v
new file mode 100644
index 0000000000..4524ae4e6f
--- /dev/null
+++ b/test-suite/primitive/sint63/asr.v
@@ -0,0 +1,41 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : (-2305843009213693952) >> 61 = -1).
+Check (eq_refl (-1) <: (-2305843009213693952) >> 61 = -1).
+Check (eq_refl (-1) <<: (-2305843009213693952) >> 61 = -1).
+Definition compute1 := Eval compute in (-2305843009213693952) >> 61.
+Check (eq_refl compute1 : -1 = -1).
+
+Check (eq_refl : 2305843009213693952 >> 62 = 0).
+Check (eq_refl 0 <: 2305843009213693952 >> 62 = 0).
+Check (eq_refl 0 <<: 2305843009213693952 >> 62 = 0).
+Definition compute2 := Eval compute in 2305843009213693952 >> 62.
+Check (eq_refl compute2 : 0 = 0).
+
+Check (eq_refl : 4611686018427387903 >> 63 = 0).
+Check (eq_refl 0 <: 4611686018427387903 >> 63 = 0).
+Check (eq_refl 0 <<: 4611686018427387903 >> 63 = 0).
+Definition compute3 := Eval compute in 4611686018427387903 >> 63.
+Check (eq_refl compute3 : 0 = 0).
+
+Check (eq_refl : (-1) >> 1 = -1).
+Check (eq_refl (-1) <: (-1) >> 1 = -1).
+Check (eq_refl (-1) <<: (-1) >> 1 = -1).
+Definition compute4 := Eval compute in (-1) >> 1.
+Check (eq_refl compute4 : -1 = -1).
+
+Check (eq_refl : (-1) >> (-1) = 0).
+Check (eq_refl 0 <: (-1) >> (-1) = 0).
+Check (eq_refl 0 <<: (-1) >> (-1) = 0).
+Definition compute5 := Eval compute in (-1) >> (-1).
+Check (eq_refl compute5 : 0 = 0).
+
+Check (eq_refl : 73 >> (-2) = 0).
+Check (eq_refl 0 <: 73 >> (-2) = 0).
+Check (eq_refl 0 <<: 73 >> (-2) = 0).
+Definition compute6 := Eval compute in 73 >> (-2).
+Check (eq_refl compute6 : 0 = 0).
diff --git a/test-suite/primitive/sint63/compare.v b/test-suite/primitive/sint63/compare.v
new file mode 100644
index 0000000000..7a9882f1c8
--- /dev/null
+++ b/test-suite/primitive/sint63/compare.v
@@ -0,0 +1,36 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 1 ?= 1 = Eq).
+Check (eq_refl Eq <: 1 ?= 1 = Eq).
+Check (eq_refl Eq <<: 1 ?= 1 = Eq).
+Definition compute1 := Eval compute in 1 ?= 1.
+Check (eq_refl compute1 : Eq = Eq).
+
+Check (eq_refl : 1 ?= 2 = Lt).
+Check (eq_refl Lt <: 1 ?= 2 = Lt).
+Check (eq_refl Lt <<: 1 ?= 2 = Lt).
+Definition compute2 := Eval compute in 1 ?= 2.
+Check (eq_refl compute2 : Lt = Lt).
+
+Check (eq_refl : 4611686018427387903 ?= 0 = Gt).
+Check (eq_refl Gt <: 4611686018427387903 ?= 0 = Gt).
+Check (eq_refl Gt <<: 4611686018427387903 ?= 0 = Gt).
+Definition compute3 := Eval compute in 4611686018427387903 ?= 0.
+Check (eq_refl compute3 : Gt = Gt).
+
+Check (eq_refl : -1 ?= 1 = Lt).
+Check (eq_refl Lt <: -1 ?= 1 = Lt).
+Check (eq_refl Lt <<: -1 ?= 1 = Lt).
+Definition compute4 := Eval compute in -1 ?= 1.
+Check (eq_refl compute4 : Lt = Lt).
+
+Check (eq_refl : 4611686018427387903 ?= -4611686018427387904 = Gt).
+Check (eq_refl Gt <: 4611686018427387903 ?= -4611686018427387904 = Gt).
+Check (eq_refl Gt <<: 4611686018427387903 ?= -4611686018427387904 = Gt).
+Definition compute5 :=
+  Eval compute in 4611686018427387903 ?= -4611686018427387904.
+Check (eq_refl compute5 : Gt = Gt).
diff --git a/test-suite/primitive/sint63/div.v b/test-suite/primitive/sint63/div.v
new file mode 100644
index 0000000000..9da628ce1e
--- /dev/null
+++ b/test-suite/primitive/sint63/div.v
@@ -0,0 +1,61 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 6 / 3 = 2).
+Check (eq_refl 2 <: 6 / 3 = 2).
+Check (eq_refl 2 <<: 6 / 3 = 2).
+Definition compute1 := Eval compute in 6 / 3.
+Check (eq_refl compute1 : 2 = 2).
+
+Check (eq_refl : -6 / 3 = -2).
+Check (eq_refl (-2) <: -6 / 3 = -2).
+Check (eq_refl (-2) <<: -6 / 3 = -2).
+Definition compute2 := Eval compute in -6 / 3.
+Check (eq_refl compute2 : -2 = -2).
+
+Check (eq_refl : 6 / -3 = -2).
+Check (eq_refl (-2) <: 6 / -3 = -2).
+Check (eq_refl (-2) <<: 6 / -3 = -2).
+Definition compute3 := Eval compute in 6 / -3.
+Check (eq_refl compute3 : -2 = -2).
+
+Check (eq_refl : -6 / -3 = 2).
+Check (eq_refl 2 <: -6 / -3 = 2).
+Check (eq_refl 2 <<: -6 / -3 = 2).
+Definition compute4 := Eval compute in -6 / -3.
+Check (eq_refl compute4 : 2 = 2).
+
+Check (eq_refl : 3 / 2 = 1).
+Check (eq_refl 1 <: 3 / 2 = 1).
+Check (eq_refl 1 <<: 3 / 2 = 1).
+Definition compute5 := Eval compute in 3 / 2.
+Check (eq_refl compute5 : 1 = 1).
+
+Check (eq_refl : -3 / 2 = -1).
+Check (eq_refl (-1) <: -3 / 2 = -1).
+Check (eq_refl (-1) <<: -3 / 2 = -1).
+Definition compute6 := Eval compute in -3 / 2.
+Check (eq_refl compute6 : -1 = -1).
+
+Check (eq_refl : 3 / -2 = -1).
+Check (eq_refl (-1) <: 3 / -2 = -1).
+Check (eq_refl (-1) <<: 3 / -2 = -1).
+Definition compute7 := Eval compute in 3 / -2.
+Check (eq_refl compute7 : -1 = -1).
+
+Check (eq_refl : -3 / -2 = 1).
+Check (eq_refl 1 <: -3 / -2 = 1).
+Check (eq_refl 1 <<: -3 / -2 = 1).
+Definition compute8 := Eval compute in -3 / -2.
+Check (eq_refl compute8 : 1 = 1).
+
+Check (eq_refl : -4611686018427387904 / -1 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <:
+  -4611686018427387904 / -1 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <<:
+  -4611686018427387904 / -1 = -4611686018427387904).
+Definition compute9 := Eval compute in -4611686018427387904 / -1.
+Check (eq_refl compute9 : -4611686018427387904 = -4611686018427387904).
diff --git a/test-suite/primitive/sint63/eqb.v b/test-suite/primitive/sint63/eqb.v
new file mode 100644
index 0000000000..4d365acf54
--- /dev/null
+++ b/test-suite/primitive/sint63/eqb.v
@@ -0,0 +1,17 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 1 =? 1 = true).
+Check (eq_refl true <: 1 =? 1 = true).
+Check (eq_refl true <<: 1 =? 1 = true).
+Definition compute1 := Eval compute in 1 =? 1.
+Check (eq_refl compute1 : true = true).
+
+Check (eq_refl : 4611686018427387903 =? 0 = false).
+Check (eq_refl false <: 4611686018427387903 =? 0 = false).
+Check (eq_refl false <<: 4611686018427387903 =? 0 = false).
+Definition compute2 := Eval compute in 4611686018427387903 =? 0.
+Check (eq_refl compute2 : false = false).
diff --git a/test-suite/primitive/sint63/isint.v b/test-suite/primitive/sint63/isint.v
new file mode 100644
index 0000000000..f1c9c2cfd1
--- /dev/null
+++ b/test-suite/primitive/sint63/isint.v
@@ -0,0 +1,50 @@
+(* This file tests the check that arithmetic operations use to know if their
+arguments are ground. The various test cases correspond to possible
+optimizations of these tests made by the compiler. *)
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Section test.
+
+Variable m n : int.
+
+Check (eq_refl : (fun x => x + 3) m = m + 3).
+Check (eq_refl (m + 3) <: (fun x => x + 3) m = m + 3).
+Check (eq_refl (m + 3) <<: (fun x => x + 3) m = m + 3).
+Definition compute1 := Eval compute in (fun x => x + 3) m.
+Check (eq_refl compute1 : m + 3 = m + 3).
+
+Check (eq_refl : (fun x => 3 + x) m = 3 + m).
+Check (eq_refl (3 + m) <: (fun x => 3 + x) m = 3 + m).
+Check (eq_refl (3 + m) <<: (fun x => 3 + x) m = 3 + m).
+Definition compute2 := Eval compute in (fun x => 3 + x) m.
+Check (eq_refl compute2 : 3 + m = 3 + m).
+
+Check (eq_refl : (fun x y => x + y) m n = m + n).
+Check (eq_refl (m + n) <: (fun x y => x + y) m n = m + n).
+Check (eq_refl (m + n) <<: (fun x y => x + y) m n = m + n).
+Definition compute3 := Eval compute in (fun x y => x + y) m n.
+Check (eq_refl compute3 : m + n = m + n).
+
+Check (eq_refl : (fun x y => x + y) 2 3 = 5).
+Check (eq_refl 5 <: (fun x y => x + y) 2 3 = 5).
+Check (eq_refl 5 <<: (fun x y => x + y) 2 3 = 5).
+Definition compute4 := Eval compute in (fun x y => x + y) 2 3.
+Check (eq_refl compute4 : 5 = 5).
+
+Check (eq_refl : (fun x => x + x) m = m + m).
+Check (eq_refl (m + m) <: (fun x => x + x) m = m + m).
+Check (eq_refl (m + m) <<: (fun x => x + x) m = m + m).
+Definition compute5 := Eval compute in (fun x => x + x) m.
+Check (eq_refl compute5 : m + m = m + m).
+
+Check (eq_refl : (fun x => x + x) 2 = 4).
+Check (eq_refl 4 <: (fun x => x + x) 2 = 4).
+Check (eq_refl 4 <<: (fun x => x + x) 2 = 4).
+Definition compute6 := Eval compute in (fun x => x + x) 2.
+Check (eq_refl compute6 : 4 = 4).
+
+End test.
diff --git a/test-suite/primitive/sint63/leb.v b/test-suite/primitive/sint63/leb.v
new file mode 100644
index 0000000000..dbe958e41d
--- /dev/null
+++ b/test-suite/primitive/sint63/leb.v
@@ -0,0 +1,29 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 1 <=? 1 = true).
+Check (eq_refl true <: 1 <=? 1 = true).
+Check (eq_refl true <<: 1 <=? 1 = true).
+Definition compute1 := Eval compute in 1 <=? 1.
+Check (eq_refl compute1 : true = true).
+
+Check (eq_refl : 1 <=? 2 = true).
+Check (eq_refl true <: 1 <=? 2 = true).
+Check (eq_refl true <<: 1 <=? 2 = true).
+Definition compute2 := Eval compute in 1 <=? 2.
+Check (eq_refl compute2 : true = true).
+
+Check (eq_refl : 4611686018427387903 <=? 0 = false).
+Check (eq_refl false <: 4611686018427387903 <=? 0 = false).
+Check (eq_refl false <<: 4611686018427387903 <=? 0 = false).
+Definition compute3 := Eval compute in 4611686018427387903 <=? 0.
+Check (eq_refl compute3 : false = false).
+
+Check (eq_refl : 1 <=? -1 = false).
+Check (eq_refl false <: 1 <=? -1 = false).
+Check (eq_refl false <<: 1 <=? -1 = false).
+Definition compute4 := Eval compute in 1 <=? -1.
+Check (eq_refl compute4 : false = false).
diff --git a/test-suite/primitive/sint63/lsl.v b/test-suite/primitive/sint63/lsl.v
new file mode 100644
index 0000000000..082c42979a
--- /dev/null
+++ b/test-suite/primitive/sint63/lsl.v
@@ -0,0 +1,43 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 3 << 61 = -2305843009213693952).
+Check (eq_refl (-2305843009213693952) <: 3 << 61 = -2305843009213693952).
+Check (eq_refl (-2305843009213693952) <<: 3 << 61 = -2305843009213693952).
+Definition compute1 := Eval compute in 3 << 61.
+Check (eq_refl compute1 : -2305843009213693952 = -2305843009213693952).
+
+Check (eq_refl : 2 << 62 = 0).
+Check (eq_refl 0 <: 2 << 62 = 0).
+Check (eq_refl 0 <<: 2 << 62 = 0).
+Definition compute2 := Eval compute in 2 << 62.
+Check (eq_refl compute2 : 0 = 0).
+
+Check (eq_refl : 4611686018427387903 << 63 = 0).
+Check (eq_refl 0 <: 4611686018427387903 << 63 = 0).
+Check (eq_refl 0 <<: 4611686018427387903 << 63 = 0).
+Definition compute3 := Eval compute in 4611686018427387903 << 63.
+Check (eq_refl compute3 : 0 = 0).
+
+Check (eq_refl : 4611686018427387903 << 62 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <:
+  4611686018427387903 << 62 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <<:
+  4611686018427387903 << 62 = -4611686018427387904).
+Definition compute4 := Eval compute in 4611686018427387903 << 62.
+Check (eq_refl compute4 : -4611686018427387904 = -4611686018427387904).
+
+Check (eq_refl : 1 << 62 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <: 1 << 62 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <<: 1 << 62 = -4611686018427387904).
+Definition compute5 := Eval compute in 1 << 62.
+Check (eq_refl compute5 : -4611686018427387904 = -4611686018427387904).
+
+Check (eq_refl : -1 << 1 = -2).
+Check (eq_refl (-2) <: -1 << 1 = -2).
+Check (eq_refl (-2) <<: -1 << 1 = -2).
+Definition compute6 := Eval compute in -1 << 1.
+Check (eq_refl compute6 : -2 = -2).
diff --git a/test-suite/primitive/sint63/ltb.v b/test-suite/primitive/sint63/ltb.v
new file mode 100644
index 0000000000..aa72e1d377
--- /dev/null
+++ b/test-suite/primitive/sint63/ltb.v
@@ -0,0 +1,29 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 1 <? 1 = false).
+Check (eq_refl false <: 1 <? 1 = false).
+Check (eq_refl false <<: 1 <? 1 = false).
+Definition compute1 := Eval compute in 1 <? 1.
+Check (eq_refl compute1 : false = false).
+
+Check (eq_refl : 1 <? 2 = true).
+Check (eq_refl true <: 1 <? 2 = true).
+Check (eq_refl true <<: 1 <? 2 = true).
+Definition compute2 := Eval compute in 1 <? 2.
+Check (eq_refl compute2 : true = true).
+
+Check (eq_refl : 4611686018427387903 <? 0 = false).
+Check (eq_refl false <: 4611686018427387903 <? 0 = false).
+Check (eq_refl false <<: 4611686018427387903 <? 0 = false).
+Definition compute3 := Eval compute in 4611686018427387903 <? 0.
+Check (eq_refl compute3 : false = false).
+
+Check (eq_refl : 1 <? -1 = false).
+Check (eq_refl false <: 1 <? -1 = false).
+Check (eq_refl false <<: 1 <? -1 = false).
+Definition compute4 := Eval compute in 1 <? -1.
+Check (eq_refl compute4 : false = false).
diff --git a/test-suite/primitive/sint63/mod.v b/test-suite/primitive/sint63/mod.v
new file mode 100644
index 0000000000..a4872b45f3
--- /dev/null
+++ b/test-suite/primitive/sint63/mod.v
@@ -0,0 +1,53 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 6 mod 3 = 0).
+Check (eq_refl 0 <: 6 mod 3 = 0).
+Check (eq_refl 0 <<: 6 mod 3 = 0).
+Definition compute1 := Eval compute in 6 mod 3.
+Check (eq_refl compute1 : 0 = 0).
+
+Check (eq_refl : -6 mod 3 = 0).
+Check (eq_refl 0 <: -6 mod 3 = 0).
+Check (eq_refl 0 <<: -6 mod 3 = 0).
+Definition compute2 := Eval compute in -6 mod 3.
+Check (eq_refl compute2 : 0 = 0).
+
+Check (eq_refl : 6 mod -3 = 0).
+Check (eq_refl 0 <: 6 mod -3 = 0).
+Check (eq_refl 0 <<: 6 mod -3 = 0).
+Definition compute3 := Eval compute in 6 mod -3.
+Check (eq_refl compute3 : 0 = 0).
+
+Check (eq_refl : -6 mod -3 = 0).
+Check (eq_refl 0 <: -6 mod -3 = 0).
+Check (eq_refl 0 <<: -6 mod -3 = 0).
+Definition compute4 := Eval compute in -6 mod -3.
+Check (eq_refl compute4 : 0 = 0).
+
+Check (eq_refl : 5 mod 3 = 2).
+Check (eq_refl 2 <: 5 mod 3 = 2).
+Check (eq_refl 2 <<: 5 mod 3 = 2).
+Definition compute5 := Eval compute in 5 mod 3.
+Check (eq_refl compute5 : 2 = 2).
+
+Check (eq_refl : -5 mod 3 = -2).
+Check (eq_refl (-2) <: -5 mod 3 = -2).
+Check (eq_refl (-2) <<: -5 mod 3 = -2).
+Definition compute6 := Eval compute in -5 mod 3.
+Check (eq_refl compute6 : -2 = -2).
+
+Check (eq_refl : 5 mod -3 = 2).
+Check (eq_refl 2 <: 5 mod -3 = 2).
+Check (eq_refl 2 <<: 5 mod -3 = 2).
+Definition compute7 := Eval compute in 5 mod -3.
+Check (eq_refl compute7 : 2 = 2).
+
+Check (eq_refl : -5 mod -3 = -2).
+Check (eq_refl (-2) <: -5 mod -3 = -2).
+Check (eq_refl (-2) <<: -5 mod -3 = -2).
+Definition compute8 := Eval compute in -5 mod -3.
+Check (eq_refl compute8 : -2 = -2).
diff --git a/test-suite/primitive/sint63/mul.v b/test-suite/primitive/sint63/mul.v
new file mode 100644
index 0000000000..f72f643083
--- /dev/null
+++ b/test-suite/primitive/sint63/mul.v
@@ -0,0 +1,35 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 2 * 3 = 6).
+Check (eq_refl 6 <: 2 * 3 = 6).
+Check (eq_refl 6 <<: 2 * 3 = 6).
+Definition compute1 := Eval compute in 2 * 3.
+Check (eq_refl compute1 : 6 = 6).
+
+Check (eq_refl : -2 * 3 = -6).
+Check (eq_refl (-6) <: -2 * 3 = -6).
+Check (eq_refl (-6) <<: -2 * 3 = -6).
+Definition compute2 := Eval compute in -2 * 3.
+Check (eq_refl compute2 : -6 = -6).
+
+Check (eq_refl : 2 * -3 = -6).
+Check (eq_refl (-6) <: 2 * -3 = -6).
+Check (eq_refl (-6) <<: 2 * -3 = -6).
+Definition compute3 := Eval compute in 2 * -3.
+Check (eq_refl compute3 : -6 = -6).
+
+Check (eq_refl : -2 * -3 = 6).
+Check (eq_refl 6 <: -2 * -3 = 6).
+Check (eq_refl 6 <<: -2 * -3 = 6).
+Definition compute4 := Eval compute in -2 * -3.
+Check (eq_refl compute4 : 6 = 6).
+
+Check (eq_refl : 4611686018427387903 * 2 = -2).
+Check (eq_refl (-2) <: 4611686018427387903 * 2 = -2).
+Check (eq_refl (-2) <<: 4611686018427387903 * 2 = -2).
+Definition compute5 := Eval compute in 4611686018427387903 * 2.
+Check (eq_refl compute5 : -2 = -2).
diff --git a/test-suite/primitive/sint63/signed.v b/test-suite/primitive/sint63/signed.v
new file mode 100644
index 0000000000..d8333a8efb
--- /dev/null
+++ b/test-suite/primitive/sint63/signed.v
@@ -0,0 +1,18 @@
+(* This file checks that operations over sint63 are signed. *)
+Require Import Sint63.
+
+Open Scope sint63_scope.
+
+(* (0-1) must be negative 1 and not the maximum integer value *)
+
+Check (eq_refl : 1/(0-1) = -1).
+Check (eq_refl (-1) <: 1/(0-1) = -1).
+Check (eq_refl (-1) <<: 1/(0-1) = -1).
+Definition compute1 := Eval compute in 1/(0-1).
+Check (eq_refl compute1 : -1 = -1).
+
+Check (eq_refl : 3 mod (0-1) = 0).
+Check (eq_refl 0 <: 3 mod (0-1) = 0).
+Check (eq_refl 0 <<: 3 mod (0-1) = 0).
+Definition compute2 := Eval compute in 3 mod (0-1).
+Check (eq_refl compute2 : 0 = 0).
diff --git a/test-suite/primitive/sint63/sub.v b/test-suite/primitive/sint63/sub.v
new file mode 100644
index 0000000000..8504177286
--- /dev/null
+++ b/test-suite/primitive/sint63/sub.v
@@ -0,0 +1,25 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 3 - 2 = 1).
+Check (eq_refl 1 <: 3 - 2 = 1).
+Check (eq_refl 1 <<: 3 - 2 = 1).
+Definition compute1 := Eval compute in 3 - 2.
+Check (eq_refl compute1 : 1 = 1).
+
+Check (eq_refl : 0 - 1 = -1).
+Check (eq_refl (-1) <: 0 - 1 = -1).
+Check (eq_refl (-1) <<: 0 - 1 = -1).
+Definition compute2 := Eval compute in 0 - 1.
+Check (eq_refl compute2 : -1 = -1).
+
+Check (eq_refl : -4611686018427387904 - 1 = 4611686018427387903).
+Check (eq_refl 4611686018427387903 <:
+  -4611686018427387904 - 1 = 4611686018427387903).
+Check (eq_refl 4611686018427387903 <<:
+  -4611686018427387904 - 1 = 4611686018427387903).
+Definition compute3 := Eval compute in -4611686018427387904 - 1.
+Check (eq_refl compute3 : 4611686018427387903 = 4611686018427387903).