diff options
| -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. |