From 34465413bc2d6b3426de783a0d35b968f7ea3b61 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 11 Nov 2014 12:20:43 +0100
Subject: Renouncing to check only at the end of the call to "apply in" the
 absence of remaining dependent evars when several arguments are given. For
 simplicity of implementation, checking instead for every step of the n-ary
 "apply in".

---
 tactics/tactics.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f8d8b09d75..6603c82cd2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1597,9 +1597,10 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
     let sigma, c = f env sigma in
-      Proofview.Unsafe.tclEVARS sigma <*>
-	(apply_in_once sidecond_first with_delta with_destruct with_evars naming id 
-	   (clear_flag,(loc,c)) tac)
+    Tacticals.New.tclWITHHOLES with_evars 
+      (apply_in_once sidecond_first with_delta with_destruct with_evars
+         naming id (clear_flag,(loc,c)))
+      sigma tac
   end
 
 (* A useful resolution tactic which, if c:A->B, transforms |- C into
-- 
cgit v1.2.3