coq-procrastination icon indicating copy to clipboard operation
coq-procrastination copied to clipboard

Published 20 hours ago • verified publisher icon Armael

Consider reimplementing everything in Ltac2

Open Armael opened this issue 7 years ago • 0 comments
trafficstars

The current implementation is relatively insane for no good reasons, except Ltac limitations. It would be interesting to see if everything can be simplified by re-implementing the library using Ltac2.

Armael avatar Jul 02 '18 16:07 Armael