From 2647f37bb4c814061190fdc8e62993acd27cfdb4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 25 Apr 2017 12:41:43 -0400 Subject: Speed up [specialize_by_assumption] --- src/Util/Tactics/SpecializeBy.v | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'src/Util/Tactics') 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. -- cgit v1.2.3