From 7ad1987d79e4338f20165940c60633dbbc8f3fe8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 21 Jul 2010 18:35:57 +0000
Subject: Fix for bug #2350 was really too quick. Here is a version that works
 better.

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

diff --git a/tactics/refine.ml b/tactics/refine.ml
index db89ec6e2e..e36859cc3a 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -263,9 +263,12 @@ let rec compute_metamap env sigma c = match kind_of_term c with
 
 let ensure_products n =
   let p = ref 0 in
-  let rec aux n =
-    if n = 0 then tclFAIL 0 (mt())
-    else tclORELSE intro (fun gl -> incr p; tclTHEN introf (aux (n-1)) gl) in
+  let rec aux n gl =
+    if n = 0 then tclFAIL 0 (mt()) gl
+    else
+      tclTHEN
+        (tclORELSE intro (fun gl -> incr p; introf gl))
+        (aux (n-1)) gl in
   tclORELSE
     (aux n)
     (* Now we know how many red are needed *)
-- 
cgit v1.2.3