From d223f85d0fd57ce74dcdcc8690a36f1ef87b408d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 21 Mar 2013 19:13:04 +0000
Subject: Using hnf instead of "intro H" for forcing reduction to a product.
 Added full betaiota in hnf. This seems more natural, even if it changes the
 strict meaning of hnf. This is source of incompatibilities as "intro" might
 succeed more often.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index bdd2bdfff7..416f0a117b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -32,6 +32,10 @@ Tactics
 - Tactic notations can now be defined locally to a module (use "Local" prefix).
 - Tactic "red" now reduces head beta-iota redexes (potential source of
   rare incompatibilities).
+- Tactic "hnf" now reduces inner beta-iota redexes
+  (potential source of rare incompatibilities).
+- Tactic "intro H" now reduces beta-iota redexes if these hide a product
+  (potential source of rare incompatibilities).
 
 Program
 
-- 
cgit v1.2.3