Depending on regular Coq-ELPI

coq-community / trocq

A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi]

http://coq-community.org/trocq/

GNU Lesser General Public License v3.0

18 stars 3 forks source link

Open palmskog opened 11 months ago

palmskog commented 11 months ago

For long-term maintenance of this project, I believe it is essential to depend on the regular Coq-ELPI.

There is a pending pull request to Coq-ELPI with the changes required: https://github.com/LPCIC/coq-elpi/pull/544