From 05c16632a3f2853006b87ed33eca2b541261aab3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 8 Dec 2016 18:11:00 +0100
Subject: [PATCH] Fix breaking ee6df099.
case H; clear H would fail when H is dependent whereas destruct H
would succeed on that, but just not clear it.
---
prelude/tactics.v | 7 +++----
1 file changed, 3 insertions(+), 4 deletions(-)
diff --git a/prelude/tactics.v b/prelude/tactics.v
index 200063102..bb13648f2 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -66,8 +66,7 @@ Ltac done :=
| discriminate
| contradiction
| split
- | match goal with H : ¬_ |- _ => case H; clear H; fast_done end
- ]
+ | match goal with H : ¬_ |- _ => case H; clear H; fast_done end ]
].
Tactic Notation "by" tactic(tac) :=
tac; done.
@@ -214,8 +213,8 @@ Tactic Notation "csimpl" "in" "*" :=
and injects equalities, and tries to contradict impossible inequalities. *)
Tactic Notation "simplify_eq" := repeat
match goal with
- | H : _ ≠_ |- _ => by case H; clear H
- | H : _ = _ → False |- _ => by case H; clear H
+ | H : _ ≠_ |- _ => by case H; try clear H
+ | H : _ = _ → False |- _ => by case H; try clear H
| H : ?x = _ |- _ => subst x
| H : _ = ?x |- _ => subst x
| H : _ = _ |- _ => discriminate H
--
GitLab