[Why3-club] Problem with the hypothesis_selection plugin

Guillaume Melquiond guillaume.melquiond at inria.fr
Tue Nov 12 13:45:45 CET 2013


On 12/11/2013 13:22, Piotr Trojanek wrote:
> I have forgot to attach the patch :(
>
> PS With hypothesis_selection enabled my goals are indeed proved.

Thanks for the patch. And I am also going to report that as a bug to the 
ocaml people, due to the sheer insanity of it.

Best regards,

Guillaume



More information about the Why3-club mailing list