Merge PR #768: Omega and romega know about context definitions (fix old bug 148)

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.