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 isCommand method incorrectly thinks that 'Notation "( x , y , .. , z )" := (pair .. (pair x y) .. ' is a complete command. It is not; the complete command is 'Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z).' It should check to make sure that not only is the final character a terminator and the next character whitespace, but that the character before the final character is not '.'.
I suspect that the code also fails to handle the 'Proof using tac. foo... bar... Qed.' style-proofs.
The text was updated successfully, but these errors were encountered:
Original report by Jason Gross (Bitbucket: jasongross9, ).
The isCommand method incorrectly thinks that 'Notation "( x , y , .. , z )" := (pair .. (pair x y) .. ' is a complete command. It is not; the complete command is 'Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z).' It should check to make sure that not only is the final character a terminator and the next character whitespace, but that the character before the final character is not '.'.
I suspect that the code also fails to handle the 'Proof using tac. foo... bar... Qed.' style-proofs.
The text was updated successfully, but these errors were encountered: