[Why3-club] Problem with the hypothesis_selection plugin
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
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."
More information about the Why3-club