diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/subtac/SubtacTactics.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v index 17ebb44117..8c8f7c43ac 100644 --- a/contrib/subtac/SubtacTactics.v +++ b/contrib/subtac/SubtacTactics.v @@ -73,3 +73,11 @@ Ltac bang := | context [False_rect _ ?p] => elim p end end. + +Ltac elim_eq_rect := + match goal with + | [ |- ?t ] => + match t with + context [ @eq_rect _ _ _ _ _ ?p ] => try case p ; simpl + end + end. |