diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-25 12:41:43 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-25 13:37:59 -0400 |
| commit | 2647f37bb4c814061190fdc8e62993acd27cfdb4 (patch) | |
| tree | edaaa6dc33cb3704d1c8584ee2de1540990d69a4 /src/Util/Tactics | |
| parent | d690e52702ef8e12e1ca908c2a0e4d80e1edd11a (diff) | |
Speed up [specialize_by_assumption]
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. |