From 1b0bd3a9e3a913a4928b68546a134a1a4448f9e8 Mon Sep 17 00:00:00 2001
From: Guillaume Bertholon
Date: Mon, 16 Jul 2018 13:30:37 +0200
Subject: Add tests for primitive floats

Add utility ldexp and frexp functions to prevent dealing with the shift of
ldshiftexp and frshiftexp everywhere.

Also move primitive integer tests to place all primitive tests in the
same directory.
---
 test-suite/arithmetic/add.v        | 18 --------------
 test-suite/arithmetic/addc.v       | 17 -------------
 test-suite/arithmetic/addcarryc.v  | 17 -------------
 test-suite/arithmetic/addmuldiv.v  | 12 ---------
 test-suite/arithmetic/compare.v    | 23 ------------------
 test-suite/arithmetic/div.v        | 17 -------------
 test-suite/arithmetic/diveucl.v    | 17 -------------
 test-suite/arithmetic/diveucl_21.v | 29 ----------------------
 test-suite/arithmetic/eqb.v        | 17 -------------
 test-suite/arithmetic/head0.v      | 23 ------------------
 test-suite/arithmetic/isint.v      | 50 --------------------------------------
 test-suite/arithmetic/land.v       | 29 ----------------------
 test-suite/arithmetic/leb.v        | 23 ------------------
 test-suite/arithmetic/lor.v        | 29 ----------------------
 test-suite/arithmetic/lsl.v        | 23 ------------------
 test-suite/arithmetic/lsr.v        | 23 ------------------
 test-suite/arithmetic/ltb.v        | 23 ------------------
 test-suite/arithmetic/lxor.v       | 29 ----------------------
 test-suite/arithmetic/mod.v        | 17 -------------
 test-suite/arithmetic/mul.v        | 17 -------------
 test-suite/arithmetic/mulc.v       | 22 -----------------
 test-suite/arithmetic/reduction.v  | 28 ---------------------
 test-suite/arithmetic/sub.v        | 17 -------------
 test-suite/arithmetic/subc.v       | 17 -------------
 test-suite/arithmetic/subcarryc.v  | 17 -------------
 test-suite/arithmetic/tail0.v      | 23 ------------------
 test-suite/arithmetic/unsigned.v   | 18 --------------
 27 files changed, 595 deletions(-)
 delete mode 100644 test-suite/arithmetic/add.v
 delete mode 100644 test-suite/arithmetic/addc.v
 delete mode 100644 test-suite/arithmetic/addcarryc.v
 delete mode 100644 test-suite/arithmetic/addmuldiv.v
 delete mode 100644 test-suite/arithmetic/compare.v
 delete mode 100644 test-suite/arithmetic/div.v
 delete mode 100644 test-suite/arithmetic/diveucl.v
 delete mode 100644 test-suite/arithmetic/diveucl_21.v
 delete mode 100644 test-suite/arithmetic/eqb.v
 delete mode 100644 test-suite/arithmetic/head0.v
 delete mode 100644 test-suite/arithmetic/isint.v
 delete mode 100644 test-suite/arithmetic/land.v
 delete mode 100644 test-suite/arithmetic/leb.v
 delete mode 100644 test-suite/arithmetic/lor.v
 delete mode 100644 test-suite/arithmetic/lsl.v
 delete mode 100644 test-suite/arithmetic/lsr.v
 delete mode 100644 test-suite/arithmetic/ltb.v
 delete mode 100644 test-suite/arithmetic/lxor.v
 delete mode 100644 test-suite/arithmetic/mod.v
 delete mode 100644 test-suite/arithmetic/mul.v
 delete mode 100644 test-suite/arithmetic/mulc.v
 delete mode 100644 test-suite/arithmetic/reduction.v
 delete mode 100644 test-suite/arithmetic/sub.v
 delete mode 100644 test-suite/arithmetic/subc.v
 delete mode 100644 test-suite/arithmetic/subcarryc.v
 delete mode 100644 test-suite/arithmetic/tail0.v
 delete mode 100644 test-suite/arithmetic/unsigned.v

(limited to 'test-suite/arithmetic')

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).
-- 
cgit v1.2.3