-
Notifications
You must be signed in to change notification settings - Fork 0
Open
Labels
Description
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.
Reactions are currently unavailable