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.
---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index fdf0c9d6be..10695b511c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -12,6 +12,9 @@ Tactics
   utility. The command "Set NativeCompute Profiling" enables
   profiling, and "Set NativeCompute Profile Filename" customizes
   the profile filename.
+- The tactic "omega" is now aware of the bodies of context variables
+  such as "x := 5 : Z" (see bug #148). This could be disabled via
+  Unset Omega UseLocalDefs.
 
 Changes from 8.7+beta1 to 8.7.0
 ===============================
-- 
cgit v1.2.3