You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The pattern is interpreted as Some (Some x); but such a syntax should not be
accepted since it suggests either that constructors are curryfied functions or
that application is right associative.
There seems to be a simple patch: to replace pattern with simple_pattern in the
grammar rule for pattern (file parsing/parser.mly, line 1053):
The ocaml grammar is accepting this:
match Some (Some 1) with Some Some x -> x
[...]
There seems to be a simple patch: to replace pattern with simple_pattern in
the
grammar rule for pattern (file parsing/parser.mly, line 1053):
J'allais dire "wow, un changement de syntaxe qui ne casse pas Coq", mais
ca casse effectivement Coq. Nous n'implementerons pas ce changement
car le nettoyage de la grammaire n'est pas une raison suffisamment
importante pour justifier un changement incompatible.
Original bug ID: 3428
Reporter: administrator
Status: closed
Resolution: won't fix
Priority: normal
Severity: feature
Category: ~DO NOT USE (was: OCaml general)
Bug description
Full_Name: Jean-Christophe Filliâtre
Version: >= 3.08.1
OS: Linux
Submission from: pc8-142.lri.fr (129.175.8.142)
The ocaml grammar is accepting this:
match Some (Some 1) with Some Some x -> x
The pattern is interpreted as Some (Some x); but such a syntax should not be
accepted since it suggests either that constructors are curryfied functions or
that application is right associative.
There seems to be a simple patch: to replace pattern with simple_pattern in the
grammar rule for pattern (file parsing/parser.mly, line 1053):
| constr_longident pattern %prec prec_constr_appl
{ mkpat(Ppat_construct($1, Some $2, false)) }
But I didn't try this patch...
Best regards,
Jean-Christophe
The text was updated successfully, but these errors were encountered: