--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on July 2019 ---
Hi frama-c team, I have tried to prove lemma by the Coq theorem prover exporting ACSL model and I have noticed the following error : /*@ axiomatic example { @type model_foo_bar = foo | bar; @ } @*/ Inductive A_model_foo_bar : Type := | C_foo : A_model_foo_bar. | C_bar : A_model_foo_bar.. Notice (dots) in the inductive A_model_foo_bar definition. It should be (dot) at the end of inductive type. Regards Dragan -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190721/60f2483b/attachment.html>