Skip to content

GitLab

Open
Created by Paolo G. Giarrusso@BlaisorbladeContributor0 of 1 task completed0/1 task

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 refine more 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]

Edited by Ralf Jung