--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on February 2020 ---
Hello, when installing Frama-C 20 there is a message that mentions that the native:coq prover is deprecated. Instead using âtipâ or âWhy-3â is suggested. I understand what using âtipâ means but I do not understand the suggestion w.r.t âWhy3â. Does this mean to use coq through Why3? If so, how is it done? Regards Jens