We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
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
exploit
H : P -> Q
Q
P
The text was updated successfully, but these errors were encountered:
No branches or pull requests
I found the
exploittactic useful in case where I haveH : P -> Qin the context or as a lemma and would like to haveQin the context with the assumptionPleft as a subgoal. The tactic is defined in: https://github.com/AbsInt/CompCert/blob/27beb944ff6ff18ea612c116e414eb40ce1320a6/lib/Coqlib.v#L57The text was updated successfully, but these errors were encountered: