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
---
 tactics/tactics.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 59e0237628..ac783adf3e 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)
-- 
cgit v1.2.3