The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
use implicit arguments for lemmas in coq_tactics.v
-
The following discussion from !338 (merged) should be addressed:
I was tempted to use implicit arguments instead of (some of) these underscores to make the
refinemore readable... does that cause problems? [@Blaisorblade]I have been thinking about this many times. However, we should not just do it locally here, but should do it globally for all proof mode tactics. First let's get #135 fixed and then do what you suggest. [@robbertkrebbers]