--- layout: fc_discuss_archives title: Message 42 from Frama-C-discuss on July 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Plateform Why3 0.72



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