From ee6df099a057ba8eb0a80ea9c03d5dcd62355d55 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Thu, 8 Dec 2016 18:00:06 +0100
Subject: [PATCH] Optimize simplify_eq.
The case tactic is faster than destruct.
---
prelude/tactics.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/prelude/tactics.v b/prelude/tactics.v
index 775393eae..200063102 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -214,8 +214,8 @@ Tactic Notation "csimpl" "in" "*" :=
and injects equalities, and tries to contradict impossible inequalities. *)
Tactic Notation "simplify_eq" := repeat
match goal with
- | H : _ ≠ _ |- _ => by destruct H
- | H : _ = _ → False |- _ => by destruct H
+ | H : _ ≠ _ |- _ => by case H; clear H
+ | H : _ = _ → False |- _ => by case H; clear H
| H : ?x = _ |- _ => subst x
| H : _ = ?x |- _ => subst x
| H : _ = _ |- _ => discriminate H
--
GitLab