The Coq mailing list

[Giulio Pellitta <gpellitta AT gmail.com>]

Dear Coq users,

I am trying to experiment a bit with the Ynot library (http://ynot.cs.harvard.edu/).

So I run coqide with the command

coqide -R /usr/lib/coq/theories/ynot Ynot Test.v &

where /usr/lib/coq/theories/ynot is the path where Ynot is installed.

When I try to run the command

Require Import Ynot.

coqide complains about the coq version:

Error: File /usr/lib/coq/theories/ynot/src/coq/Ynot.vo has bad magic number.
It is corrupted or was compiled with another version of Coq.

Indeed, I am running Coq 8.4pl5, but the latest version of Ynot available on http://ynot.cs.harvard.edu/ is only for version 8.3pl2.

Is there any way for me to use Ynot with my version of Coq?

Best,
Giulio Pellitta