coq-tricks

coq-tricks copied to clipboard

I found the exploit tactic useful in case where I have H : P -> Q in the context or as a lemma and would like to have Q in the context with the assumption P left as a subgoal. The tactic is defined in: https://github.com/AbsInt/CompCert/blob/27beb944ff6ff18ea612c116e414eb40ce1320a6/lib/Coqlib.v#L57