diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Init/Tactics.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 6aa1198c08..a4347bbe62 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -233,6 +233,7 @@ Tactic Notation "clear" "dependent" hyp(h) := clear h || match goal with | H : context [ h ] |- _ => depclear H; depclear h + | H := context [ h ] |- _ => depclear H; depclear h end || fail "hypothesis to clear is used in the conclusion (maybe indirectly)" in depclear h. |