[Why3-club] Compilation error with coq8.4

Virgile Prevosto virgile.prevosto at m4x.org
Tue Sep 4 15:50:50 CEST 2012


2012/8/28 Jean-Christophe Filliatre <Jean-Christophe.Filliatre at lri.fr>:
> On 28/08/2012 12:29, Jean Fortin wrote:
>>
>> Hello, when trying to install why3-0.73, I get the following error at
>> compilation:
>>
>> 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
>>
>> I have coq 8.4 installed.
>> Is this a known issue?
>
>
> Yes (Why3 0.73 is not compatible with Coq 8.4).
>

FWIW, here is a patch that let Why3 compile against Coq 8.4
(Disclaimer: it has not been extensively tested). It can also be found
in Godi's apps-why3 package (http://godi.camlcity.org/godi/index.html)

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
-------------- section suivante --------------
Une pi?ce jointe autre que texte a ?t? nettoy?e...
Nom: patch-aa-coq-8.4-compat
Type: application/octet-stream
Taille: 4138 octets
Desc: non disponible
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20120904/9ed43aed/attachment.obj>


More information about the Why3-club mailing list