--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on January 2010 ---
to use coq within Frama-C/Jessie, you cannot use gwhy. Instead frama-c -jessie -jessie-atp coq file.c should generate file.jessie/coq/file_why.v and you can fill-in proofs as usual with Coq, e.g coqide file.jessie/coq/file_why.v - claude Groleo Marius wrote: > Hi, > I have coq 8.2 and why 2.18 on ubuntu 9.10. > > When I try to prove some code with coq, I get the following message in > the console. > Thread 1 killed on uncaught exception Failure("For interactive > provers, option --project must be set") > > How can I get around this issue ? > > Thanks. >