From fd364b7e0934872e4ac1f9ffa01ec27c2330cc75 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 8 Dec 2016 17:05:01 +0100
Subject: [PATCH] Avoid exponential blowup in [done] as caused by a7e91677.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Example:

Goal
  ¬False → ¬False → ¬False → ¬False → ¬False → ¬False → ¬False →
  False.
Proof.
  intros. done. (* takes very long *)
---
 prelude/tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/prelude/tactics.v b/prelude/tactics.v
index 7ca9b524a..775393eae 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -66,7 +66,7 @@ Ltac done :=
     | discriminate
     | contradiction
     | split
-    | match goal with H : ¬_ |- _ => case H; clear H; done end
+    | match goal with H : ¬_ |- _ => case H; clear H; fast_done end
     ]
   ].
 Tactic Notation "by" tactic(tac) :=
-- 
GitLab