diff options
Diffstat (limited to 'test-suite/bugs/closed/1362.v')
-rw-r--r-- | test-suite/bugs/closed/1362.v | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/1362.v b/test-suite/bugs/closed/1362.v new file mode 100644 index 00000000..6cafb9f0 --- /dev/null +++ b/test-suite/bugs/closed/1362.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. |