4 files changed, 18 insertions, 36 deletions
diff --git a/test-suite/arithmetic/diveucl_21.v b/test-suite/arithmetic/diveucl_21.v
index 7e12a08906..b888c97be3 100644
--- a/test-suite/arithmetic/diveucl_21.v
+++ b/test-suite/arithmetic/diveucl_21.v
@@ -15,3 +15,11 @@ Check (eq_refl (4611686018427387904, 1) <: diveucl_21 3 1 2 = (46116860184273879
 Check (eq_refl (4611686018427387904, 1) <<: diveucl_21 3 1 2 = (4611686018427387904, 1)).
 Definition compute2 := Eval compute in diveucl_21 3 1 2.
 Check (eq_refl compute2 : (4611686018427387904, 1) = (4611686018427387904, 1)).
+
+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)).
diff --git a/test-suite/bugs/closed/bug_10031.v b/test-suite/bugs/closed/bug_10031.v
new file mode 100644
index 0000000000..15b53de00d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10031.v
@@ -0,0 +1,9 @@
+Require Import Int63 ZArith.
+
+Open Scope int63_scope.
+
+Goal False.
+cut (let (q, r) := (0, 0) in ([|q|], [|r|]) = (9223372036854775808%Z, 0%Z));
+  [discriminate| ].
+Fail (change (0, 0) with (diveucl_21 1 0 1); apply diveucl_21_spec).
+Abort.
diff --git a/test-suite/output/Error_msg_diffs.v b/test-suite/output/Error_msg_diffs.v
index 11c766b210..a26e683398 100644
--- a/test-suite/output/Error_msg_diffs.v
+++ b/test-suite/output/Error_msg_diffs.v
@@ -1,4 +1,4 @@
-(* coq-prog-args: ("-color" "on" "-async-proofs" "off") *)
+(* coq-prog-args: ("-color" "on" "-diffs" "on" "-async-proofs" "off") *)
 (* Re: -async-proofs off, see https://github.com/coq/coq/issues/9671 *)
 (* Shows diffs in an error message for an "Unable to unify" error *)
 Require Import Arith List Bool.
diff --git a/test-suite/success/ROmega3.v b/test-suite/success/ROmega3.v
deleted file mode 100644
index ef9cb17b4b..0000000000
--- a/test-suite/success/ROmega3.v
+++ /dev/null
@@ -1,35 +0,0 @@
-
-Require Import ZArith Lia.
-Local Open Scope Z_scope.
-
-(** Benchmark provided by Chantal Keller, that romega used to
-    solve far too slowly (compared to omega or lia). *)
-
-(* In Coq 8.9 (end of 2018), the `romega` tactics are deprecated.
-   The tests in this file remain but now call the `lia` tactic. *)
-
-
-Parameter v4 : Z.
-Parameter v3 : Z.
-Parameter o4 : Z.
-Parameter s5 : Z.
-Parameter v2 : Z.
-Parameter o5 : Z.
-Parameter s6 : Z.
-Parameter v1 : Z.
-Parameter o6 : Z.
-Parameter s7 : Z.
-Parameter v0 : Z.
-Parameter o7 : Z.
-
-Lemma lemma_5833 :
- ~ 16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 +
-      (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 +
-         (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 8192
-\/
-  16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 +
-      (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 +
-         (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 1024.
-Proof.
-Timeout 1 lia. (* should take a few milliseconds, not seconds *)
-Timeout 1 Qed. (* ditto *)