18.8 Bugs

There is no discharge mechanism for programs; so you cannot do a program's proof inside a section (actually, you can do it, but your program will not exist anymore after having closed the section).

Surely there are still many bugs in this implementation. Please send bug reports to Jean-Christophe.Filliatre@lri.fr. Don't forget to send the version of Coq used (given by coqtop -v) and a script producing the bug.