--- layout: fc_discuss_archives title: Message 42 from Frama-C-discuss on July 2012 ---
Le lundi 23 juillet 2012 ? 16:09 +0200, DAHAN Mickael a ?crit : > During the installation of Why3 O.72 the following problems appear: > ./configure --enable-coq-plugin --enable-coq-libs > Coq support : yes > Version : 8.4beta2 > Ocamlopt src/coq-tactic/why3tac.ml > File "src/coq-tactic/why3tac.ml", line 477, characters 14-20: > Error: This pattern matches values of type 'a option > but a pattern was expected which matches values of type > Declarations.constant_def > make: *** [src/coq-tactic/why3tac.cmx] Error 2 [CCing the Why3 mailing-list, since it doesn't have much to do with Frama-C] I would suggest that you either disable the Coq plugin or use a 8.3 version of Coq. Presumably, you will also encounter issues when compiling Coq libraries for Why3, since Coq 8.3 is the only version being currently tested extensively. Best regards, Guillaume