2 files changed, 13 insertions, 35 deletions
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 *)
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index a9821b027f..2f676cf9ad 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -68,3 +68,16 @@ eassumption.
 match goal with |- ?x=1 => change (x=1) with (0+x=1) end.
 match goal with |- 0+1=1 => trivial end.
 Qed.
+
+(* Mini-check that no_check does not check *)
+
+Goal True -> False.
+intro H.
+change_no_check nat.
+apply S.
+change_no_check nat with bool.
+change_no_check nat in H.
+change_no_check nat with (bool->bool) in H.
+exact (H true).
+Fail Qed.
+Abort.