From 427a99c4af46d3113c18f09c0d7d12e00feb7031 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 11 Apr 2016 16:52:51 +0200
Subject: [PATCH] Use (more primitive) case instead of destruct in done tactic.

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

diff --git a/prelude/tactics.v b/prelude/tactics.v
index 970982061..a9c3458e6 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -56,7 +56,7 @@ Ltac done :=
     | contradiction
     | solve [apply not_symmetry; trivial]
     | split ]
-  | match goal with H : ¬_ |- _ => solve [destruct H; trivial] end ].
+  | match goal with H : ¬_ |- _ => solve [case H; trivial] end ].
 Tactic Notation "by" tactic(tac) :=
   tac; done.
 
-- 
GitLab