diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-13 12:21:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-23 12:57:48 +0100 |
| commit | 446b265f5d1f6e6828a7f653b1f648ebdf768321 (patch) | |
| tree | 97e5ac9077264c774e871b201137ae4871100a34 /test-suite/bugs | |
| parent | 1b09c7b0802c85ea72931720a7cb4fbf9ab5e211 (diff) | |
Recognizing Z in romega up to conversion.
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 4562ed1f1..1507fa4bf 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. |