diff options
Diffstat (limited to 'src/Util/Tactics')
-rw-r--r-- | src/Util/Tactics/SpecializeBy.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/Util/Tactics/SpecializeBy.v b/src/Util/Tactics/SpecializeBy.v index 72cf5d52f..3abd58195 100644 --- a/src/Util/Tactics/SpecializeBy.v +++ b/src/Util/Tactics/SpecializeBy.v @@ -29,5 +29,10 @@ Tactic Notation "specialize_by" tactic3(tac) := specialize_by tac. (** A marginally faster version of [specialize_by assumption] *) Ltac specialize_by_assumption := repeat match goal with - | [ H : ?T, H' : (?T -> ?U)%type |- _ ] => specialize (H' H) + | [ H : ?T, H' : (?T -> ?U)%type |- _ ] + => lazymatch goal with + | [ _ : context[H'] |- _ ] => fail + | [ |- context[H'] ] => fail + | _ => specialize (H' H) + end end. |