diff options
| author | Pierre Letouzey | 2017-06-12 11:34:53 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2017-10-05 23:30:05 +0200 |
| commit | 87a63ffc6dd36be0ef2e757b46f3c81f67f96207 (patch) | |
| tree | ef900a9277584b91e436eaebecdef31779fc58f4 /test-suite | |
| parent | 2aac4ae818fec0d409da31ef9da83796d871d687 (diff) | |
Omega now aware of context variables with bodies (in type Z or nat) (fix bug 148)
For compatibility, this extra feature of omega could be disabled via
Unset Omega UseLocalDefs.
Caveat : for now, real let-ins inside goals or hyps aren't handled, use
some "cbv zeta" reduction if you want to get rid of them. And context
definitions whose types aren't Z or nat are ignored, some manual "unfold"
are still mandatory if expanding these definitions will help omega.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/148.v | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/148.v b/test-suite/bugs/closed/148.v new file mode 100644 index 0000000000..6cafb9f0cd --- /dev/null +++ b/test-suite/bugs/closed/148.v @@ -0,0 +1,26 @@ +(** Omega is now aware of the bodies of context variables + (of type Z or nat). *) + +Require Import ZArith Omega. +Open Scope Z. + +Goal let x := 3 in x = 3. +intros. +omega. +Qed. + +Open Scope nat. + +Goal let x := 2 in x = 2. +intros. +omega. +Qed. + +(** NB: this could be disabled for compatibility reasons *) + +Unset Omega UseLocalDefs. + +Goal let x := 4 in x = 4. +intros. +Fail omega. +Abort. |