Forked from
Iris / Iris
Source project has a limited visibility.
-
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).
Armaël Guéneau authoredWith 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.