From aa2a39fa7d754aaf3270dc0bed3128822254e8d1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 19 Jun 2011 14:12:34 +0000
Subject: Ensured that the transparency state is used when flag betaiota is on
 for apply. + small typo fix in r14217 + added compatibility of betaiota flag
 with 8.3 when "-compat 8.3" is given

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14223 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 90d8b604f1..54b44309e8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -35,7 +35,7 @@ Tactics
 - Tactic (and Eval command) vm_compute can now be interrupted via Ctrl-C.
 - Unification in "apply" supports unification of patterns of the form
   ?f x y = g(x,y) (compatibility ensured by using
-  "Unset Tactic Pattern Unification").
+  "Unset Tactic Pattern Unification"). It also supports (full) betaiota.
 - Tactic autorewrite does no longer instantiate pre-existing
   existential variables (theoretical source of possible incompatibility).
 
-- 
cgit v1.2.3