diff options
| author | Pierre-Marie Pédrot | 2020-03-19 12:31:18 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-19 12:31:18 +0100 |
| commit | 1d8698e97dee385151ef92efd924560b296f8d50 (patch) | |
| tree | ffa306a04b70d5facb1ed046579a769f5843dc7d /theories | |
| parent | b69b87ce35b09b164929974b85b815d259185f18 (diff) | |
| parent | 40c830beaad34a9ad435816da11fb93322368478 (diff) | |
Merge PR #11822: Grants #11692: clear dependent knows about let-in
Reviewed-by: JasonGross
Reviewed-by: ppedrot
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. |