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]