Coq-Elpi 1.13.0 for Coq 8.15
This release requires Elpi 1.14.0 and provides improved performances especially with code generating many evars.
The API now provides access to Hint Resolve
, Hint Opaque
and (simple) functor declaration/application.
The vernacular command Accumulate
can now load files from Coq's loadpath, which does not depend on the current working directory (since proof general and vscoq disagree on that).