FStar
FStar copied to clipboard
Forbid `//` in operators
trafficstars
Hi,
As discussed last Monday, this PR, subsequent of #2666, changes the lexer so that the sequence // is forbidden in operators. The string ++//* used to be lexed as the operator ++//*, now it is lexed as the operator ++ and the comment //*.