• Armaël Guéneau's avatar
    Optimize iIntoEmpValid · 20b0a19d
    Armaël Guéneau authored
    With large proof contexts and lemmas with many forall quantifiers,
    iIntoEmpValid can become quite slow. This makes it go faster by adding
    "fast paths" for the -> and forall cases, gated by Ltac pattern
    matching (which is faster than trying to unify with refine and fail).
To find the state of this project's repository at the time of any of these versions, check out the tags.