diff options
Diffstat (limited to 'test-suite/bugs/closed/bug_1912.v')
| -rw-r--r-- | test-suite/bugs/closed/bug_1912.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/bug_1912.v b/test-suite/bugs/closed/bug_1912.v index 0228abbb9b..9f6c8177f6 100644 --- a/test-suite/bugs/closed/bug_1912.v +++ b/test-suite/bugs/closed/bug_1912.v @@ -1,6 +1,6 @@ -Require Import Omega. +Require Import Lia ZArith. Goal forall x, Z.succ (Z.pred x) = x. intros x. -omega. +lia. Qed. |