diff options
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/4717.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4717.v b/test-suite/bugs/closed/4717.v index 4562ed1f1a..1507fa4bf0 100644 --- a/test-suite/bugs/closed/4717.v +++ b/test-suite/bugs/closed/4717.v @@ -19,7 +19,7 @@ Proof. omega. Qed. -Require Import ZArith. +Require Import ZArith ROmega. Open Scope Z_scope. @@ -32,4 +32,6 @@ Theorem Zle_not_eq_lt : forall n m, Proof. intros. omega. + Undo. + romega. Qed. |