Commit 05c16632 by Robbert Krebbers

### 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.```
parent fa3141d2
 ... @@ -66,8 +66,7 @@ Ltac done := ... @@ -66,8 +66,7 @@ Ltac done := | discriminate | discriminate | contradiction | contradiction | split | 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) := Tactic Notation "by" tactic(tac) := tac; done. tac; done. ... @@ -214,8 +213,8 @@ Tactic Notation "csimpl" "in" "*" := ... @@ -214,8 +213,8 @@ Tactic Notation "csimpl" "in" "*" := and injects equalities, and tries to contradict impossible inequalities. *) and injects equalities, and tries to contradict impossible inequalities. *) Tactic Notation "simplify_eq" := repeat Tactic Notation "simplify_eq" := repeat match goal with match goal with | H : _ ≠ _ |- _ => by case H; clear H | H : _ ≠ _ |- _ => by case H; try clear H | H : _ = _ → False |- _ => by case H; clear H | H : _ = _ → False |- _ => by case H; try clear H | H : ?x = _ |- _ => subst x | H : ?x = _ |- _ => subst x | H : _ = ?x |- _ => subst x | H : _ = ?x |- _ => subst x | H : _ = _ |- _ => discriminate H | H : _ = _ |- _ => discriminate H ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!