Incompatibility with Coq < 8.15

ecranceMERCE / trakt

A generic goal preprocessing tool for proof automation tactics in Coq

https://ecrancemerce.github.io/trakt

GNU Lesser General Public License v3.0

14 stars 7 forks source link

Incompatibility with Coq < 8.15 #7

Open pi8027 opened 2 years ago

pi8027 commented 2 years ago

commands.elpi uses coq.option.set, which is available from Coq-Elpi 1.12.0 for Coq 8.15, despite the fact that the OPAM file indicates that Trakt is compatible with Coq >= 8.13. Incidentally, it would be nice to have CI.

ckeller commented 2 years ago

Hi For SMTCoq and Sniper, we do need a version running with Coq 8.13, which includes commit 50c0f3e0b1f27a0216718b4c00c73de5f9bb9d45 ;-) I have prepared something like this here: https://github.com/ckeller/trakt/tree/1.1+50c0f3e . Thanks!