From 8c1e25acc561767980acdccc987087f51e0e2a12 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:41:07 +0000
Subject: Tacticals.New.tclWITHHOLES: clean up.

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

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index f25bae9bb8..fe527a811d 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -512,7 +512,7 @@ module New = struct
           try
             Refiner.check_evars env new_sigma sigma initial_sigma;
             tclUNIT ()
-          with e ->
+          with e when Errors.noncritical e ->
             tclZERO e
         in
         let check_evars_if =
@@ -523,7 +523,7 @@ module New = struct
           else
             tclUNIT ()
         in
-        Proofview.V82.tactic (Refiner.tclEVARS sigma) <*> tac x <*> check_evars_if
+        Proofview.V82.tclEVARS sigma <*> tac x <*> check_evars_if
 
   let tclTIMEOUT n t =
     Proofview.tclOR
-- 
cgit v1.2.3