diff options
Diffstat (limited to 'test-suite/bugs/closed/bug_4132.v')
| -rw-r--r-- | test-suite/bugs/closed/bug_4132.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/bug_4132.v b/test-suite/bugs/closed/bug_4132.v index 67ecc3087f..2ebbb66758 100644 --- a/test-suite/bugs/closed/bug_4132.v +++ b/test-suite/bugs/closed/bug_4132.v @@ -1,5 +1,5 @@ -Require Import ZArith Omega. +Require Import ZArith Lia. Open Scope Z_scope. (** bug 4132: omega was using "simpl" either on whole equations, or on @@ -14,18 +14,18 @@ Lemma foo (H : - zxy' <= zxy) (H' : zxy' <= x') : - b <= zxy. Proof. -omega. (* was: Uncaught exception Invalid_argument("index out of bounds"). *) +lia. (* was: Uncaught exception Invalid_argument("index out of bounds"). *) Qed. Lemma foo2 x y (b := 5) (H1 : x <= y) (H2 : y <= b) : x <= b. -omega. (* Pierre L: according to a comment of bug report #4132, +lia. (* Pierre L: according to a comment of bug report #4132, this might have triggered "index out of bounds" in the past, but I never managed to reproduce that in any version, even before my fix. *) Qed. Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b. -omega. (* Pierre L: according to a comment of bug report #4132, +lia. (* Pierre L: according to a comment of bug report #4132, this might have triggered "Failure(occurrence 2)" in the past, but I never managed to reproduce that. *) Qed. |