Move elpi code to a .elpi file

math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components

33 stars 2 forks source link

Closed gares closed 3 years ago

gares commented 3 years ago

This has two advantages:

works also with proof general
Elpi Accumulate File supports #[skip] and #[only] which may help in the future to achieve compatibility with different Coq versions

Note: files mentioned in Elpi Accumulate File are part of the .vo file, so nothing has to be done in make install