[Why3-club] Problem with the hypothesis_selection plugin

François Bobot francois.bobot at cea.fr
Tue Nov 12 16:54:03 CET 2013


On 12/11/2013 13:45, Guillaume Melquiond wrote:
> On 12/11/2013 13:22, Piotr Trojanek wrote:
>> I have forgot to attach the patch :(

Thanks for 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.
>

I'm not sure ocaml is the only to blame, "let _ =" is a bad pratice 
especially when the type is unit, if you write instead "let () =" ocaml 
says:

Error: This expression has type desc:Why3.Pp.formatted -> unit
        but an expression was expected of type unit

But I agree that ocaml should fired the warning 5 in such a case:
"Partially applied function: expression whose result has  function  type
and is ignored."

-- 
François




More information about the Why3-club mailing list