From 87a63ffc6dd36be0ef2e757b46f3c81f67f96207 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 12 Jun 2017 11:34:53 +0200
Subject: 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.
---
 test-suite/bugs/closed/148.v | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 test-suite/bugs/closed/148.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3