From 792a07d519a8dd396674e5431af2380a26d74b9c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 2 Jun 2013 21:31:30 +0000
Subject: Fixing buggy backtracking in "intros * pat" with failing "pat".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16549 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0595a7789a..44bc4df1f7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -490,11 +490,12 @@ let intros = tclREPEAT intro
 let intro_erasing id = tclTHEN (thin [id]) (introduction id)
 
 let intro_forthcoming_then_gen loc name_flag move_flag dep_flag tac =
-  let rec aux ids =
-    tclORELSE0
-      (intro_then_gen loc name_flag  move_flag false dep_flag
-         (fun id -> aux (id::ids)))
-      (tac ids) in
+  let rec aux ids gl =
+    try
+      intro_then_gen loc name_flag  move_flag false dep_flag
+         (fun id -> aux (id::ids)) gl
+    with RefinerError IntroNeedsProduct ->
+      tac ids gl in
   aux []
 
 let rec get_next_hyp_position id = function
-- 
cgit v1.2.3