[Why3-club] Coq driver

Guillaume Melquiond guillaume.melquiond at inria.fr
Tue Mar 18 11:54:42 CET 2014

On 18/03/2014 06:17, Guillaume Melquiond wrote:
> A possible fix is to move the type constraints from the polymorphic type
> definitions to the polymorphic function definitions. That would fix the
> issue above, but I don't know yet if that won't break something else.

And this is the fix that is now implemented in the master of why3.

Best regards,


More information about the Why3-club mailing list