From 0a6e65e3cec0a8f00f357d82489532203f315389 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Wed, 15 Feb 2017 13:18:40 -0500
Subject: address some code review comments

---
 src/Util/Tactics.v | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'src/Util/Tactics.v')

diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index 5f7ad65cc..d98ac1bd4 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -32,11 +32,12 @@ Ltac debuglevel := constr:(0%nat).
 
 Ltac solve_debugfail tac :=
   solve [tac] ||
-        let dbg := debuglevel in
-        match dbg with
-        | O => idtac
-        | _ => match goal with |- ?G => idtac "couldn't prove" G end
-        end.
+        ( let dbg := debuglevel in
+          match dbg with
+          | O => idtac
+          | _ => match goal with |- ?G => idtac "couldn't prove" G end
+          end;
+          fail).
 
 Ltac set_evars :=
   repeat match goal with
-- 
cgit v1.2.3