From ecd4c983d94ffc3a22a5d043e615d40e55bad033 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 15 Apr 2012 22:05:54 +0000
Subject: In "intro until" and its applications, be consistent when reduction
 is used or not before trying to introduce.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15175 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0f23d512f2..e4ac2a5bc7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -552,7 +552,7 @@ let depth_of_quantified_hypothesis red h gl =
 	  str".")
 
 let intros_until_gen red h g =
-  tclDO (depth_of_quantified_hypothesis red h g) intro g
+  tclDO (depth_of_quantified_hypothesis red h g) (if red then introf else intro) g
 
 let intros_until_id id = intros_until_gen true (NamedHyp id)
 let intros_until_n_gen red n = intros_until_gen red (AnonHyp n)
-- 
cgit v1.2.3