Gospel does not parse `fun` type annotations as OCaml

[shym]

The following code is accepted by the OCaml type checker:

  fun true : int -> 12

(besides the obviously non-exhaustive pattern true), meaning that the int is the return type but the Gospel typechecker accepts the following:

val f : int list -> int
(*@ y = f xs
    ensures List.for_all (fun x : int -> true) xs *)

where int is interpreted as the type for the argument x.

[shym]

309 will change that situation:

val f : int list -> int
(*@ y = f xs
    ensures List.for_all (fun x : int -> true) xs *)

will now report a syntax error at : int as the type annotation is not handled by the parser.

[n-osborne]

Fixed by #309