diff options
Diffstat (limited to 'test-suite/bugs/closed/bug_1362.v')
| -rw-r--r-- | test-suite/bugs/closed/bug_1362.v | 15 |
1 files changed, 3 insertions, 12 deletions
diff --git a/test-suite/bugs/closed/bug_1362.v b/test-suite/bugs/closed/bug_1362.v index 6cafb9f0cd..18b8d743b3 100644 --- a/test-suite/bugs/closed/bug_1362.v +++ b/test-suite/bugs/closed/bug_1362.v @@ -1,26 +1,17 @@ (** Omega is now aware of the bodies of context variables (of type Z or nat). *) -Require Import ZArith Omega. +Require Import ZArith Lia. Open Scope Z. Goal let x := 3 in x = 3. intros. -omega. +lia. Qed. Open Scope nat. Goal let x := 2 in x = 2. intros. -omega. +lia. Qed. - -(** NB: this could be disabled for compatibility reasons *) - -Unset Omega UseLocalDefs. - -Goal let x := 4 in x = 4. -intros. -Fail omega. -Abort. |