From d223f85d0fd57ce74dcdcc8690a36f1ef87b408d Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
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
---
 doc/refman/RefMan-tac.tex | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'doc/refman/RefMan-tac.tex')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index a2d02a4ca..4f4c88d01 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -671,8 +671,8 @@ H}{\it n} or {\tt X}{\it n} is a fresh identifier.
 In both cases, the new subgoal is $U$.
 
 If the goal is neither a product nor starting with a let definition,
-the tactic {\tt intro} applies the tactic {\tt red} until the tactic
-{\tt intro} can be applied or the goal is not reducible.
+the tactic {\tt intro} applies the tactic {\tt hnf} until the tactic
+{\tt intro} can be applied or the goal is not head-reducible.
 
 \begin{ErrMsgs}
 \item \errindex{No product even after head-reduction}
@@ -2916,7 +2916,8 @@ $\beta\iota\zeta$-reduction rules.
 This tactic applies to any goal. It replaces the current goal with its
 head normal form according to the $\beta\delta\iota\zeta$-reduction
 rules, i.e.  it reduces the head of the goal until it becomes a
-product or an irreducible term.
+product or an irreducible term. All inner $\beta\iota$-redexes are also
+reduced.
 
 \Example
 The term \verb+forall n:nat, (plus (S n) (S n))+ is not reduced by {\tt hnf}.
-- 
cgit v1.2.3

