diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-29 12:24:34 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-29 12:24:34 -0700 |
| commit | ad90f29cf77dc5f29a04941480a862f2f06923c2 (patch) | |
| tree | 7f5015ed72f3b528336023356aec03086e889ce8 /src/Util/HProp.v | |
| parent | 8cdbaf69e02f5784b392adb99abc89d2be663ad2 (diff) | |
Remove some lemmas that make things slower in Util/HProp
Diffstat (limited to 'src/Util/HProp.v')
| -rw-r--r-- | src/Util/HProp.v | 2 |
1 files changed, 0 insertions, 2 deletions
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. |