From ad90f29cf77dc5f29a04941480a862f2f06923c2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 29 Jul 2016 12:24:34 -0700 Subject: Remove some lemmas that make things slower in Util/HProp --- src/Util/HProp.v | 2 -- 1 file changed, 2 deletions(-) (limited to 'src/Util') diff --git a/src/Util/HProp.v b/src/Util/HProp.v index 63de1d037..b85797176 100644 --- a/src/Util/HProp.v +++ b/src/Util/HProp.v @@ -17,8 +17,6 @@ Ltac hprop_destruct_trivial_step := => destruct (H x0 x1) | [ H : forall a0 (x y : _), x = y, x0 : ?A, x1 : ?A |- _ ] => destruct (H _ x0 x1) - | [ H : or _ _ |- _ ] => destruct H - | [ H : sum _ _ |- _ ] => destruct H end. Ltac hprop_destruct_trivial := repeat hprop_destruct_trivial_step. -- cgit v1.2.3