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

6 files changed, 32 insertions, 21 deletions

diff --git a/CHANGES b/CHANGES
index bdd2bdfff..416f0a117 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
 
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}.
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 86195edd2..508569f0d 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -812,7 +812,7 @@ let try_red_product env sigma c =
 
 let red_product env sigma c =
   try try_red_product env sigma c
-  with Redelimination -> error "Not reducible."
+  with Redelimination -> error "No head constant to reduce."
 
 (*
 (* This old version of hnf uses betadeltaiota instead of itself (resp
@@ -882,8 +882,9 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
               | CoFix _ | Fix _ -> s'
 	      | _ -> redrec (applist(c, stack)))
 	| None -> s'
-    else s'
-  in applist (redrec c)
+    else s' in
+  let simpfun = clos_norm_flags betaiota env sigma in
+  simpfun (applist (redrec c))
 
 let hnf_constr = whd_simpl_orelse_delta_but_fix
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 59e023762..ac783adf3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -443,9 +443,9 @@ let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac gl =
         (* that intro do betaiotazeta only when reduction is needed; and *)
         (* probably also a pity that intro does zeta *)
 	try
-	  tclTHEN try_red_in_concl
-	    (intro_then_gen loc name_flag move_flag force_flag dep_flag tac) gl
-	with Redelimination ->
+	  tclTHEN hnf_in_concl
+	    (intro_then_gen loc name_flag move_flag false dep_flag tac) gl
+	with RefinerError IntroNeedsProduct ->
 	  user_err_loc(loc,"Intro",str "No product even after head-reduction.")
 
 let intro_gen loc n m f d = intro_then_gen loc n m f d (fun _ -> tclIDTAC)
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index 3599da4dc..25e0ec2f7 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -3,5 +3,22 @@
 
 Goal forall A, A -> True.
 intros _ _.
+Abort.
 
+(* This did not work until March 2013, because of underlying "red" *)
+Goal (fun x => True -> True) 0.
+intro H.
+Abort.
+
+(* This should still work, with "intro" calling "hnf" *)
+Goal (fun f => True -> f 0 = f 0) (fun x => x).
+intro H.
+match goal with [ |- 0 = 0 ] => reflexivity end.
+Abort.
+
+(* Somewhat related: This did not work until March 2013 *)
+Goal (fun f => f 0 = f 0) (fun x => x).
+hnf.
+match goal with [ |- 0 = 0 ] => reflexivity end.
+Abort.
 
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index 2252e42fc..6f02ac9f5 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -93,21 +93,9 @@ Program Instance all_iff_morphism {A : Type} :
 Program Instance all_impl_morphism {A : Type} :
   Proper (pointwise_relation A impl ==> impl) (@all A) | 1.
 
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation, all in *.
-    intuition ; specialize (H x0) ; intuition.
-  Qed.
-
 Program Instance all_inverse_impl_morphism {A : Type} :
   Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@all A) | 1.
 
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation, all in *.
-    intuition ; specialize (H x0) ; intuition.
-  Qed.
-
 (** Equivalent points are simultaneously accessible or not *)
 
 Instance Acc_pt_morphism {A:Type}(E R : A->A->Prop)