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.

21 files changed, 607 insertions, 17 deletions

diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out
index 7ca4de1e46..96af456891 100644
--- a/test-suite/output/Int63Syntax.out
+++ b/test-suite/output/Int63Syntax.out
@@ -15,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.PrimInt63.int
+Cannot interpret this number as a value of type int
 The command has indeed failed with message:
-Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int
+Cannot interpret this number as a value of type int
 0
      : int
 0
@@ -33,9 +33,11 @@ The reference x was not found in the current environment.
 add 2 2
      : int
 The command has indeed failed with message:
-int63 are only non-negative numbers.
+Cannot interpret this number as a value of type int
 The command has indeed failed with message:
 overflow in int63 literal: 9223372036854775808
+0x1
+     : int
 2
      : nat
 2%int63
diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v
index 50910264f2..be0ee701af 100644
--- a/test-suite/output/Int63Syntax.v
+++ b/test-suite/output/Int63Syntax.v
@@ -20,6 +20,11 @@ Fail Check 0x.
 Check (PrimInt63.add 2 2).
 Fail Check -1.
 Fail Check 9223372036854775808.
+
+Set Printing All.
+Check 1%int63.
+Unset Printing All.
+
 Open Scope nat_scope.
 Check 2. (* : nat *)
 Check 2%int63.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 3477a293e3..0b18981f4e 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -77,18 +77,18 @@ fun x : nat => [x]
      : nat -> nat
 ∀ x : nat, x = x
      : Prop
-File "stdin", line 184, characters 0-160:
+File "stdin", line 187, characters 0-160:
 Warning: Notation "∀ _ .. _ , _" was already defined with a different format
 in scope type_scope. [notation-incompatible-format,parsing]
 ∀x : nat,x = x
      : Prop
-File "stdin", line 197, characters 0-60:
+File "stdin", line 200, characters 0-60:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 201, characters 0-64:
+File "stdin", line 204, characters 0-64:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 206, characters 0-62:
+File "stdin", line 209, characters 0-62:
 Warning: Lonely notation "_ %%%% _" was already defined with a different
 format. [notation-incompatible-format,parsing]
 3  %%  4
@@ -97,10 +97,10 @@ format. [notation-incompatible-format,parsing]
      : nat
 3   %%   4
      : nat
-File "stdin", line 234, characters 0-61:
+File "stdin", line 237, characters 0-61:
 Warning: The format modifier is irrelevant for only parsing rules.
 [irrelevant-format-only-parsing,parsing]
-File "stdin", line 238, characters 0-63:
+File "stdin", line 241, characters 0-63:
 Warning: The only parsing modifier has no effect in Reserved Notation.
 [irrelevant-reserved-notation-only-parsing,parsing]
 fun x : nat => U (S x)
@@ -111,7 +111,7 @@ fun x : nat => V x
      : forall x : nat, nat * (?T -> ?T)
 where
 ?T : [x : nat  x0 : ?T |- Type] (x0 cannot be used)
-File "stdin", line 255, characters 0-30:
+File "stdin", line 258, characters 0-30:
 Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing]
 0 :=: 0
      : Prop
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index ebad12af88..a5ec92fe3c 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -103,7 +103,10 @@ Module NumberNotations.
     Delimit Scope test17_scope with test17.
     Local Set Primitive Projections.
     Record myint63 := of_int { to_int : int }.
-    Number Notation myint63 of_int to_int : test17_scope.
+    Definition parse x :=
+      match x with Pos x => Some (of_int x) | Neg _ => None end.
+    Definition print x := Pos (to_int x).
+    Number Notation myint63 parse print : test17_scope.
     Check let v := 0%test17 in v : myint63.
   End Test17.
 End NumberNotations.
diff --git a/test-suite/output/NumberNotations.out b/test-suite/output/NumberNotations.out
index 60682edec8..df9b39389c 100644
--- a/test-suite/output/NumberNotations.out
+++ b/test-suite/output/NumberNotations.out
@@ -260,28 +260,28 @@ The command has indeed failed with message:
 add is not a constructor of an inductive type.
 The command has indeed failed with message:
 Missing mapping for constructor Iempty.
-File "stdin", line 574, characters 56-61:
+File "stdin", line 577, characters 56-61:
 Warning: Type of I'sum seems incompatible with the type of sum.
 Expected type is: (I' -> I' -> I') instead of (I -> I' -> I').
 This might yield ill typed terms when using the notation.
 [via-type-mismatch,numbers]
-File "stdin", line 579, characters 32-33:
+File "stdin", line 582, characters 32-33:
 Warning: I was already mapped to Set, mapping it also to
 nat might yield ill typed terms when using the notation.
 [via-type-remapping,numbers]
-File "stdin", line 579, characters 37-42:
+File "stdin", line 582, characters 37-42:
 Warning: Type of Iunit seems incompatible with the type of O.
 Expected type is: I instead of I.
 This might yield ill typed terms when using the notation.
 [via-type-mismatch,numbers]
 The command has indeed failed with message:
 'via' and 'abstract' cannot be used together.
-File "stdin", line 659, characters 21-23:
+File "stdin", line 662, characters 21-23:
 Warning: Type of I1 seems incompatible with the type of Fin.F1.
 Expected type is: (nat -> I) instead of I.
 This might yield ill typed terms when using the notation.
 [via-type-mismatch,numbers]
-File "stdin", line 659, characters 35-37:
+File "stdin", line 662, characters 35-37:
 Warning: Type of IS seems incompatible with the type of Fin.FS.
 Expected type is: (nat -> I -> I) instead of (I -> I).
 This might yield ill typed terms when using the notation.
diff --git a/test-suite/output/NumberNotations.v b/test-suite/output/NumberNotations.v
index 718da13500..85400c2fd4 100644
--- a/test-suite/output/NumberNotations.v
+++ b/test-suite/output/NumberNotations.v
@@ -328,7 +328,10 @@ Module Test17.
   Delimit Scope test17_scope with test17.
   Local Set Primitive Projections.
   Record myint63 := of_int { to_int : int }.
-  Number Notation myint63 of_int to_int : test17_scope.
+  Definition parse x :=
+    match x with Pos x => Some (of_int x) | Neg _ => None end.
+  Definition print x := Pos (to_int x).
+  Number Notation myint63 parse print : test17_scope.
   Check let v := 0%test17 in v : myint63.
 End Test17.
 
diff --git a/test-suite/output/Sint63Syntax.out b/test-suite/output/Sint63Syntax.out
new file mode 100644
index 0000000000..db14658307
--- /dev/null
+++ b/test-suite/output/Sint63Syntax.out
@@ -0,0 +1,66 @@
+2%sint63
+     : int
+2
+     : int
+-3
+     : int
+4611686018427387903
+     : int
+-4611686018427387904
+     : int
+427
+     : int
+427
+     : int
+427
+     : int
+427
+     : int
+427
+     : int
+The command has indeed failed with message:
+Cannot interpret this number as a value of type int
+The command has indeed failed with message:
+Cannot interpret this number as a value of type int
+0
+     : int
+0
+     : int
+The command has indeed failed with message:
+The reference xg was not found in the current environment.
+The command has indeed failed with message:
+The reference xG was not found in the current environment.
+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
+The command has indeed failed with message:
+Cannot interpret this number as a value of type int
+The command has indeed failed with message:
+Cannot interpret this number as a value of type int
+0x1%int63
+     : int
+0x7fffffffffffffff%int63
+     : int
+2
+     : nat
+2%sint63
+     : int
+t = 2%si63
+     : int
+t = 2%si63
+     : int
+2
+     : nat
+2
+     : int
+(2 + 2)%sint63
+     : int
+2 + 2
+     : int
+     = 4
+     : int
+     = 37151199385380486
+     : int
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.
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).