Merge PR #9867: Add primitive floats (binary64 floating-point numbers)

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl

27 files changed, 0 insertions, 595 deletions

diff --git a/test-suite/arithmetic/add.v b/test-suite/arithmetic/add.v
deleted file mode 100644
index fb7eb1d53c..0000000000
--- a/test-suite/arithmetic/add.v
+++ /dev/null
@@ -1,18 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_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 : 9223372036854775807 + 1 = 0).
-Check (eq_refl 0 <: 9223372036854775807 + 1 = 0).
-Check (eq_refl 0 <<: 9223372036854775807 + 1 = 0).
-Definition compute2 := Eval compute in 9223372036854775807 + 1.
-Check (eq_refl compute2 : 0 = 0).
diff --git a/test-suite/arithmetic/addc.v b/test-suite/arithmetic/addc.v
deleted file mode 100644
index 432aec0291..0000000000
--- a/test-suite/arithmetic/addc.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_scope.
-
-Check (eq_refl : 2 +c 3 = C0 5).
-Check (eq_refl (C0 5) <: 2 +c 3 = C0 5).
-Check (eq_refl (C0 5) <<: 2 +c 3 = C0 5).
-Definition compute1 := Eval compute in 2 +c 3.
-Check (eq_refl compute1 : C0 5 = C0 5).
-
-Check (eq_refl : 9223372036854775807 +c 2 = C1 1).
-Check (eq_refl (C1 1) <: 9223372036854775807 +c 2 = C1 1).
-Check (eq_refl (C1 1) <<: 9223372036854775807 +c 2 = C1 1).
-Definition compute2 := Eval compute in 9223372036854775807 +c 2.
-Check (eq_refl compute2 : C1 1 = C1 1).
diff --git a/test-suite/arithmetic/addcarryc.v b/test-suite/arithmetic/addcarryc.v
deleted file mode 100644
index a4430769ca..0000000000
--- a/test-suite/arithmetic/addcarryc.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_scope.
-
-Check (eq_refl : addcarryc 2 3 = C0 6).
-Check (eq_refl (C0 6) <: addcarryc 2 3 = C0 6).
-Check (eq_refl (C0 6) <<: addcarryc 2 3 = C0 6).
-Definition compute1 := Eval compute in addcarryc 2 3.
-Check (eq_refl compute1 : C0 6 = C0 6).
-
-Check (eq_refl : addcarryc 9223372036854775807 2 = C1 2).
-Check (eq_refl (C1 2) <: addcarryc 9223372036854775807 2 = C1 2).
-Check (eq_refl (C1 2) <<: addcarryc 9223372036854775807 2 = C1 2).
-Definition compute2 := Eval compute in addcarryc 9223372036854775807 2.
-Check (eq_refl compute2 : C1 2 = C1 2).
diff --git a/test-suite/arithmetic/addmuldiv.v b/test-suite/arithmetic/addmuldiv.v
deleted file mode 100644
index 72b0164b49..0000000000
--- a/test-suite/arithmetic/addmuldiv.v
+++ /dev/null
@@ -1,12 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_scope.
-
-Check (eq_refl : addmuldiv 32 3 5629499534213120 = 12887523328).
-Check (eq_refl 12887523328 <: addmuldiv 32 3 5629499534213120 = 12887523328).
-Check (eq_refl 12887523328 <<: addmuldiv 32 3 5629499534213120 = 12887523328).
-
-Definition compute2 := Eval compute in addmuldiv 32 3 5629499534213120.
-Check (eq_refl compute2 : 12887523328 = 12887523328).
diff --git a/test-suite/arithmetic/compare.v b/test-suite/arithmetic/compare.v
deleted file mode 100644
index a8d1ea1226..0000000000
--- a/test-suite/arithmetic/compare.v
+++ /dev/null
@@ -1,23 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_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 : 9223372036854775807 ?= 0 = Gt).
-Check (eq_refl Gt <: 9223372036854775807 ?= 0 = Gt).
-Check (eq_refl Gt <<: 9223372036854775807 ?= 0 = Gt).
-Definition compute3 := Eval compute in 9223372036854775807 ?= 0.
-Check (eq_refl compute3 : Gt = Gt).
diff --git a/test-suite/arithmetic/div.v b/test-suite/arithmetic/div.v
deleted file mode 100644
index 0ee0b91580..0000000000
--- a/test-suite/arithmetic/div.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_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 : 3 / 2 = 1).
-Check (eq_refl 1 <: 3 / 2 = 1).
-Check (eq_refl 1 <<: 3 / 2 = 1).
-Definition compute2 := Eval compute in 3 / 2.
-Check (eq_refl compute2 : 1 = 1).
diff --git a/test-suite/arithmetic/diveucl.v b/test-suite/arithmetic/diveucl.v
deleted file mode 100644
index 8f88a0f356..0000000000
--- a/test-suite/arithmetic/diveucl.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_scope.
-
-Check (eq_refl : diveucl 6 3 = (2,0)).
-Check (eq_refl (2,0) <: diveucl 6 3 = (2,0)).
-Check (eq_refl (2,0) <<: diveucl 6 3 = (2,0)).
-Definition compute1 := Eval compute in diveucl 6 3.
-Check (eq_refl compute1 : (2,0) = (2,0)).
-
-Check (eq_refl : diveucl 5 3 = (1,2)).
-Check (eq_refl (1,2) <: diveucl 5 3 = (1,2)).
-Check (eq_refl (1,2) <<: diveucl 5 3 = (1,2)).
-Definition compute2 := Eval compute in diveucl 5 3.
-Check (eq_refl compute2 : (1,2) = (1,2)).
diff --git a/test-suite/arithmetic/diveucl_21.v b/test-suite/arithmetic/diveucl_21.v
deleted file mode 100644
index b12dba429c..0000000000
--- a/test-suite/arithmetic/diveucl_21.v
+++ /dev/null
@@ -1,29 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_scope.
-
-Check (eq_refl : diveucl_21 1 1 2 = (4611686018427387904,1)).
-Check (eq_refl (4611686018427387904,1) <: diveucl_21 1 1 2 = (4611686018427387904,1)).
-Check (eq_refl (4611686018427387904,1) <<: diveucl_21 1 1 2 = (4611686018427387904,1)).
-Definition compute1 := Eval compute in diveucl_21 1 1 2.
-Check (eq_refl compute1 : (4611686018427387904,1) = (4611686018427387904,1)).
-
-Check (eq_refl : diveucl_21 3 1 2 = (0, 0)).
-Check (eq_refl (0, 0) <: diveucl_21 3 1 2 = (0, 0)).
-Check (eq_refl (0, 0) <<: diveucl_21 3 1 2 = (0, 0)).
-Definition compute2 := Eval compute in diveucl_21 3 1 2.
-Check (eq_refl compute2 : (0, 0) = (0, 0)).
-
-Check (eq_refl : diveucl_21 1 1 0 = (0,0)).
-Check (eq_refl (0,0) <: diveucl_21 1 1 0 = (0,0)).
-Check (eq_refl (0,0) <<: diveucl_21 1 1 0 = (0,0)).
-
-Check (eq_refl : diveucl_21 9223372036854775807 0 1 = (0,0)).
-Check (eq_refl (0,0) <: diveucl_21 9223372036854775807 0 1 = (0,0)).
-Check (eq_refl (0,0) <<: diveucl_21 9223372036854775807 0 1 = (0,0)).
-
-Check (eq_refl : diveucl_21 9305446873517 1793572051078448654 4930380657631323783 = (17407905077428, 3068214991893055266)).
-Check (eq_refl (17407905077428, 3068214991893055266) <: diveucl_21 9305446873517 1793572051078448654 4930380657631323783 = (17407905077428, 3068214991893055266)).
-Check (eq_refl (17407905077428, 3068214991893055266) <<: diveucl_21 9305446873517 1793572051078448654 4930380657631323783 = (17407905077428, 3068214991893055266)).
diff --git a/test-suite/arithmetic/eqb.v b/test-suite/arithmetic/eqb.v
deleted file mode 100644
index dcc0b71f6d..0000000000
--- a/test-suite/arithmetic/eqb.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_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 : 9223372036854775807 == 0 = false).
-Check (eq_refl false <: 9223372036854775807 == 0 = false).
-Check (eq_refl false <<: 9223372036854775807 == 0 = false).
-Definition compute2 := Eval compute in 9223372036854775807 == 0.
-Check (eq_refl compute2 : false = false).
diff --git a/test-suite/arithmetic/head0.v b/test-suite/arithmetic/head0.v
deleted file mode 100644
index f4234d2605..0000000000
--- a/test-suite/arithmetic/head0.v
+++ /dev/null
@@ -1,23 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_scope.
-
-Check (eq_refl : head0 3 = 61).
-Check (eq_refl 61 <: head0 3 = 61).
-Check (eq_refl 61 <<: head0 3 = 61).
-Definition compute1 := Eval compute in head0 3.
-Check (eq_refl compute1 : 61 = 61).
-
-Check (eq_refl : head0 4611686018427387904 = 0).
-Check (eq_refl 0 <: head0 4611686018427387904 = 0).
-Check (eq_refl 0 <<: head0 4611686018427387904 = 0).
-Definition compute2 := Eval compute in head0 4611686018427387904.
-Check (eq_refl compute2 : 0 = 0).
-
-Check (eq_refl : head0 0 = 63).
-Check (eq_refl 63 <: head0 0 = 63).
-Check (eq_refl 63 <<: head0 0 = 63).
-Definition compute3 := Eval compute in head0 0.
-Check (eq_refl compute3 : 63 = 63).
diff --git a/test-suite/arithmetic/isint.v b/test-suite/arithmetic/isint.v
deleted file mode 100644
index c215caa878..0000000000
--- a/test-suite/arithmetic/isint.v
+++ /dev/null
@@ -1,50 +0,0 @@
-(* 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 Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_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/arithmetic/land.v b/test-suite/arithmetic/land.v
deleted file mode 100644
index 0ea6fd90b6..0000000000
--- a/test-suite/arithmetic/land.v
+++ /dev/null
@@ -1,29 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_scope.
-
-Check (eq_refl : 0 land 0 = 0).
-Check (eq_refl 0 <: 0 land 0 = 0).
-Check (eq_refl 0 <<: 0 land 0 = 0).
-Definition compute1 := Eval compute in 0 land 0.
-Check (eq_refl compute1 : 0 = 0).
-
-Check (eq_refl : 9223372036854775807 land 0 = 0).
-Check (eq_refl 0 <: 9223372036854775807 land 0 = 0).
-Check (eq_refl 0 <<: 9223372036854775807 land 0 = 0).
-Definition compute2 := Eval compute in 9223372036854775807 land 0.
-Check (eq_refl compute2 : 0 = 0).
-
-Check (eq_refl : 0 land 9223372036854775807 = 0).
-Check (eq_refl 0 <: 0 land 9223372036854775807 = 0).
-Check (eq_refl 0 <<: 0 land 9223372036854775807 = 0).
-Definition compute3 := Eval compute in 0 land 9223372036854775807.
-Check (eq_refl compute3 : 0 = 0).
-
-Check (eq_refl : 9223372036854775807 land 9223372036854775807 = 9223372036854775807).
-Check (eq_refl 9223372036854775807 <: 9223372036854775807 land 9223372036854775807 = 9223372036854775807).
-Check (eq_refl 9223372036854775807 <<: 9223372036854775807 land 9223372036854775807 = 9223372036854775807).
-Definition compute4 := Eval compute in 9223372036854775807 land 9223372036854775807.
-Check (eq_refl compute4 : 9223372036854775807 = 9223372036854775807).
diff --git a/test-suite/arithmetic/leb.v b/test-suite/arithmetic/leb.v
deleted file mode 100644
index 5354919978..0000000000
--- a/test-suite/arithmetic/leb.v
+++ /dev/null
@@ -1,23 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_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 : 9223372036854775807 <= 0 = false).
-Check (eq_refl false <: 9223372036854775807 <= 0 = false).
-Check (eq_refl false <<: 9223372036854775807 <= 0 = false).
-Definition compute3 := Eval compute in 9223372036854775807 <= 0.
-Check (eq_refl compute3 : false = false).
diff --git a/test-suite/arithmetic/lor.v b/test-suite/arithmetic/lor.v
deleted file mode 100644
index 9c3b85c054..0000000000
--- a/test-suite/arithmetic/lor.v
+++ /dev/null
@@ -1,29 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_scope.
-
-Check (eq_refl : 0 lor 0 = 0).
-Check (eq_refl 0 <: 0 lor 0 = 0).
-Check (eq_refl 0 <<: 0 lor 0 = 0).
-Definition compute1 := Eval compute in 0 lor 0.
-Check (eq_refl compute1 : 0 = 0).
-
-Check (eq_refl : 9223372036854775807 lor 0 = 9223372036854775807).
-Check (eq_refl 9223372036854775807 <: 9223372036854775807 lor 0 = 9223372036854775807).
-Check (eq_refl 9223372036854775807 <<: 9223372036854775807 lor 0 = 9223372036854775807).
-Definition compute2 := Eval compute in 9223372036854775807 lor 0.
-Check (eq_refl compute2 : 9223372036854775807 = 9223372036854775807).
-
-Check (eq_refl : 0 lor 9223372036854775807 = 9223372036854775807).
-Check (eq_refl 9223372036854775807 <: 0 lor 9223372036854775807 = 9223372036854775807).
-Check (eq_refl 9223372036854775807 <<: 0 lor 9223372036854775807 = 9223372036854775807).
-Definition compute3 := Eval compute in 0 lor 9223372036854775807.
-Check (eq_refl compute3 : 9223372036854775807 = 9223372036854775807).
-
-Check (eq_refl : 9223372036854775807 lor 9223372036854775807 = 9223372036854775807).
-Check (eq_refl 9223372036854775807 <: 9223372036854775807 lor 9223372036854775807 = 9223372036854775807).
-Check (eq_refl 9223372036854775807 <<: 9223372036854775807 lor 9223372036854775807 = 9223372036854775807).
-Definition compute4 := Eval compute in 9223372036854775807 lor 9223372036854775807.
-Check (eq_refl compute4 : 9223372036854775807 = 9223372036854775807).
diff --git a/test-suite/arithmetic/lsl.v b/test-suite/arithmetic/lsl.v
deleted file mode 100644
index 70f3b90140..0000000000
--- a/test-suite/arithmetic/lsl.v
+++ /dev/null
@@ -1,23 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_scope.
-
-Check (eq_refl : 3 << 61 = 6917529027641081856).
-Check (eq_refl 6917529027641081856 <: 3 << 61 = 6917529027641081856).
-Check (eq_refl 6917529027641081856 <<: 3 << 61 = 6917529027641081856).
-Definition compute1 := Eval compute in 3 << 61.
-Check (eq_refl compute1 : 6917529027641081856 = 6917529027641081856).
-
-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 : 9223372036854775807 << 64 = 0).
-Check (eq_refl 0 <: 9223372036854775807 << 64 = 0).
-Check (eq_refl 0 <<: 9223372036854775807 << 64 = 0).
-Definition compute3 := Eval compute in 9223372036854775807 << 64.
-Check (eq_refl compute3 : 0 = 0).
diff --git a/test-suite/arithmetic/lsr.v b/test-suite/arithmetic/lsr.v
deleted file mode 100644
index c36c24e237..0000000000
--- a/test-suite/arithmetic/lsr.v
+++ /dev/null
@@ -1,23 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_scope.
-
-Check (eq_refl : 6917529027641081856 >> 61 = 3).
-Check (eq_refl 3 <: 6917529027641081856 >> 61 = 3).
-Check (eq_refl 3 <<: 6917529027641081856 >> 61 = 3).
-Definition compute1 := Eval compute in 6917529027641081856 >> 61.
-Check (eq_refl compute1 : 3 = 3).
-
-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 : 9223372036854775807 >> 64 = 0).
-Check (eq_refl 0 <: 9223372036854775807 >> 64 = 0).
-Check (eq_refl 0 <<: 9223372036854775807 >> 64 = 0).
-Definition compute3 := Eval compute in 9223372036854775807 >> 64.
-Check (eq_refl compute3 : 0 = 0).
diff --git a/test-suite/arithmetic/ltb.v b/test-suite/arithmetic/ltb.v
deleted file mode 100644
index 7ae5ac6493..0000000000
--- a/test-suite/arithmetic/ltb.v
+++ /dev/null
@@ -1,23 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_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 : 9223372036854775807 < 0 = false).
-Check (eq_refl false <: 9223372036854775807 < 0 = false).
-Check (eq_refl false <<: 9223372036854775807 < 0 = false).
-Definition compute3 := Eval compute in 9223372036854775807 < 0.
-Check (eq_refl compute3 : false = false).
diff --git a/test-suite/arithmetic/lxor.v b/test-suite/arithmetic/lxor.v
deleted file mode 100644
index b453fc7697..0000000000
--- a/test-suite/arithmetic/lxor.v
+++ /dev/null
@@ -1,29 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_scope.
-
-Check (eq_refl : 0 lxor 0 = 0).
-Check (eq_refl 0 <: 0 lxor 0 = 0).
-Check (eq_refl 0 <<: 0 lxor 0 = 0).
-Definition compute1 := Eval compute in 0 lxor 0.
-Check (eq_refl compute1 : 0 = 0).
-
-Check (eq_refl : 9223372036854775807 lxor 0 = 9223372036854775807).
-Check (eq_refl 9223372036854775807 <: 9223372036854775807 lxor 0 = 9223372036854775807).
-Check (eq_refl 9223372036854775807 <<: 9223372036854775807 lxor 0 = 9223372036854775807).
-Definition compute2 := Eval compute in 9223372036854775807 lxor 0.
-Check (eq_refl compute2 : 9223372036854775807 = 9223372036854775807).
-
-Check (eq_refl : 0 lxor 9223372036854775807 = 9223372036854775807).
-Check (eq_refl 9223372036854775807 <: 0 lxor 9223372036854775807 = 9223372036854775807).
-Check (eq_refl 9223372036854775807 <<: 0 lxor 9223372036854775807 = 9223372036854775807).
-Definition compute3 := Eval compute in 0 lxor 9223372036854775807.
-Check (eq_refl compute3 : 9223372036854775807 = 9223372036854775807).
-
-Check (eq_refl : 9223372036854775807 lxor 9223372036854775807 = 0).
-Check (eq_refl 0 <: 9223372036854775807 lxor 9223372036854775807 = 0).
-Check (eq_refl 0 <<: 9223372036854775807 lxor 9223372036854775807 = 0).
-Definition compute4 := Eval compute in 9223372036854775807 lxor 9223372036854775807.
-Check (eq_refl compute4 : 0 = 0).
diff --git a/test-suite/arithmetic/mod.v b/test-suite/arithmetic/mod.v
deleted file mode 100644
index 5307eed493..0000000000
--- a/test-suite/arithmetic/mod.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_scope.
-
-Check (eq_refl : 6 \% 3 = 0).
-Check (eq_refl 0 <: 6 \% 3 = 0).
-Check (eq_refl 0 <<: 6 \% 3 = 0).
-Definition compute1 := Eval compute in 6 \% 3.
-Check (eq_refl compute1 : 0 = 0).
-
-Check (eq_refl : 5 \% 3 = 2).
-Check (eq_refl 2 <: 5 \% 3 = 2).
-Check (eq_refl 2 <<: 5 \% 3 = 2).
-Definition compute2 := Eval compute in 5 \% 3.
-Check (eq_refl compute2 : 2 = 2).
diff --git a/test-suite/arithmetic/mul.v b/test-suite/arithmetic/mul.v
deleted file mode 100644
index 9480e8cd46..0000000000
--- a/test-suite/arithmetic/mul.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_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 : 9223372036854775807 * 2 = 9223372036854775806).
-Check (eq_refl 9223372036854775806 <: 9223372036854775807 * 2 = 9223372036854775806).
-Check (eq_refl 9223372036854775806 <<: 9223372036854775807 * 2 = 9223372036854775806).
-Definition compute2 := Eval compute in 9223372036854775807 * 2.
-Check (eq_refl compute2 : 9223372036854775806 = 9223372036854775806).
diff --git a/test-suite/arithmetic/mulc.v b/test-suite/arithmetic/mulc.v
deleted file mode 100644
index e10855bafa..0000000000
--- a/test-suite/arithmetic/mulc.v
+++ /dev/null
@@ -1,22 +0,0 @@
-Require Import Cyclic63.
-
-Set Implicit Arguments.
-
-Open Scope int63_scope.
-
-Check (eq_refl : 2 *c 3 = WW 0 6).
-Check (eq_refl (WW 0 6) <: 2 *c 3 = WW 0 6).
-Check (eq_refl (WW 0 6) <<: 2 *c 3 = WW 0 6).
-Definition compute1 := Eval compute in 2 *c 3.
-Check (eq_refl compute1 : WW 0 6 = WW 0 6).
-
-Check (eq_refl : 9223372036854775807 *c 2 = WW 1 9223372036854775806).
-Check (eq_refl (WW 1 9223372036854775806) <: 9223372036854775807 *c 2 = WW 1 9223372036854775806).
-Check (eq_refl (WW 1 9223372036854775806) <<: 9223372036854775807 *c 2 = WW 1 9223372036854775806).
-
-Definition compute2 := Eval compute in 9223372036854775807 *c 2.
-Check (eq_refl compute2 : WW 1 9223372036854775806 = WW 1 9223372036854775806).
-
-Check (eq_refl : 0 *c 0 = W0).
-Check (eq_refl (@W0 int) <: 0 *c 0 = W0).
-Check (eq_refl (@W0 int) <<: 0 *c 0 = W0).
diff --git a/test-suite/arithmetic/reduction.v b/test-suite/arithmetic/reduction.v
deleted file mode 100644
index 00e067ac5a..0000000000
--- a/test-suite/arithmetic/reduction.v
+++ /dev/null
@@ -1,28 +0,0 @@
-Require Import Int63.
-
-Open Scope int63_scope.
-
-Definition div_eucl_plus_one i1 i2 :=
-  let (q,r) := diveucl i1 i2 in
-  (q+1, r+1)%int63.
-
-Definition rcbn := Eval cbn in div_eucl_plus_one 3 2.
-Check (eq_refl : rcbn = (2, 2)).
-
-Definition rcbv := Eval cbv in div_eucl_plus_one 3 2.
-Check (eq_refl : rcbv = (2, 2)).
-
-Definition rvmc := Eval vm_compute in div_eucl_plus_one 3 2.
-Check (eq_refl : rvmc = (2, 2)).
-
-Definition f n m :=
-  match (n ?= 42)%int63 with
-  | Lt => (n + m)%int63
-  | _ => (2*m)%int63
-  end.
-
-Goal forall n, (n ?= 42)%int63 = Gt -> f n 256 = 512%int63.
-  intros. unfold f.
-  cbn. Undo. cbv. (* Test reductions under match clauses *)
-  rewrite H. reflexivity.
-Qed.
diff --git a/test-suite/arithmetic/sub.v b/test-suite/arithmetic/sub.v
deleted file mode 100644
index 1606fd2aa1..0000000000
--- a/test-suite/arithmetic/sub.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_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 = 9223372036854775807).
-Check (eq_refl 9223372036854775807 <: 0 - 1 = 9223372036854775807).
-Check (eq_refl 9223372036854775807 <<: 0 - 1 = 9223372036854775807).
-Definition compute2 := Eval compute in 0 - 1.
-Check (eq_refl compute2 : 9223372036854775807 = 9223372036854775807).
diff --git a/test-suite/arithmetic/subc.v b/test-suite/arithmetic/subc.v
deleted file mode 100644
index fc4067e48b..0000000000
--- a/test-suite/arithmetic/subc.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_scope.
-
-Check (eq_refl : 3 -c 2 = C0 1).
-Check (eq_refl (C0 1) <: 3 -c 2 = C0 1).
-Check (eq_refl (C0 1) <<: 3 -c 2 = C0 1).
-Definition compute1 := Eval compute in 3 -c 2.
-Check (eq_refl compute1 : C0 1 = C0 1).
-
-Check (eq_refl : 0 -c 1 = C1 9223372036854775807).
-Check (eq_refl (C1 9223372036854775807) <: 0 -c 1 = C1 9223372036854775807).
-Check (eq_refl (C1 9223372036854775807) <<: 0 -c 1 = C1 9223372036854775807).
-Definition compute2 := Eval compute in 0 -c 1.
-Check (eq_refl compute2 : C1 9223372036854775807 = C1 9223372036854775807).
diff --git a/test-suite/arithmetic/subcarryc.v b/test-suite/arithmetic/subcarryc.v
deleted file mode 100644
index e81b6536b2..0000000000
--- a/test-suite/arithmetic/subcarryc.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_scope.
-
-Check (eq_refl : subcarryc 3 1 = C0 1).
-Check (eq_refl (C0 1) <: subcarryc 3 1 = C0 1).
-Check (eq_refl (C0 1) <<: subcarryc 3 1 = C0 1).
-Definition compute1 := Eval compute in subcarryc 3 1.
-Check (eq_refl compute1 : C0 1 = C0 1).
-
-Check (eq_refl : subcarryc 0 1 = C1 9223372036854775806).
-Check (eq_refl (C1 9223372036854775806) <: subcarryc 0 1 = C1 9223372036854775806).
-Check (eq_refl (C1 9223372036854775806) <<: subcarryc 0 1 = C1 9223372036854775806).
-Definition compute2 := Eval compute in subcarryc 0 1.
-Check (eq_refl compute2 : C1 9223372036854775806 = C1 9223372036854775806).
diff --git a/test-suite/arithmetic/tail0.v b/test-suite/arithmetic/tail0.v
deleted file mode 100644
index c9d426087a..0000000000
--- a/test-suite/arithmetic/tail0.v
+++ /dev/null
@@ -1,23 +0,0 @@
-Require Import Int63.
-
-Set Implicit Arguments.
-
-Open Scope int63_scope.
-
-Check (eq_refl : tail0 2305843009213693952 = 61).
-Check (eq_refl 61 <: tail0 2305843009213693952 = 61).
-Check (eq_refl 61 <<: tail0 2305843009213693952 = 61).
-Definition compute1 := Eval compute in tail0 2305843009213693952.
-Check (eq_refl compute1 : 61 = 61).
-
-Check (eq_refl : tail0 1 = 0).
-Check (eq_refl 0 <: tail0 1 = 0).
-Check (eq_refl 0 <<: tail0 1 = 0).
-Definition compute2 := Eval compute in tail0 1.
-Check (eq_refl compute2 : 0 = 0).
-
-Check (eq_refl : tail0 0 = 63).
-Check (eq_refl 63 <: tail0 0 = 63).
-Check (eq_refl 63 <<: tail0 0 = 63).
-Definition compute3 := Eval compute in tail0 0.
-Check (eq_refl compute3 : 63 = 63).
diff --git a/test-suite/arithmetic/unsigned.v b/test-suite/arithmetic/unsigned.v
deleted file mode 100644
index 82920bd201..0000000000
--- a/test-suite/arithmetic/unsigned.v
+++ /dev/null
@@ -1,18 +0,0 @@
-(* This file checks that operations over int63 are unsigned. *)
-Require Import Int63.
-
-Open Scope int63_scope.
-
-(* (0-1) must be the maximum integer value and not negative 1 *)
-
-Check (eq_refl : 1/(0-1) = 0).
-Check (eq_refl 0 <: 1/(0-1) = 0).
-Check (eq_refl 0 <<: 1/(0-1) = 0).
-Definition compute1 := Eval compute in 1/(0-1).
-Check (eq_refl compute1 : 0 = 0).
-
-Check (eq_refl : 3 \% (0-1) = 3).
-Check (eq_refl 3 <: 3 \% (0-1) = 3).
-Check (eq_refl 3 <<: 3 \% (0-1) = 3).
-Definition compute2 := Eval compute in 3 \% (0-1).
-Check (eq_refl compute2 : 3 = 3).