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

1 files changed, 4 insertions, 3 deletions

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}.