From 6c72e455a048d69048ddf386c43d5fc5eb4597a4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 25 Aug 2014 13:55:03 +0200
Subject: Fixing previous commit.

---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 407f367ed9..7e6e960a64 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1339,7 +1339,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
           Tacticals.New.tclTHEN
             (apply_clear_request clear_flag false c)
             (tac id))
-    with e when with_destruct && when Errors.noncritical e ->
+    with e when with_destruct && Errors.noncritical e ->
       let e = Errors.push e in
       descend_in_conjunctions aux (fun _ -> raise e) c
     end
-- 
cgit v1.2.3