The Coq mailing list

[Stefan Monnier <monnier AT iro.umontreal.ca>]

> It's known to compile with both coq 8.1 and 8.2 using coqc on the
> command line.  Note that you won't be able to step through it in proof
> general or coqide, though, because it depends on a feature they don't
> implement.

Looks like you forgot to add the margin in your attachment,


        Stefan