parser bug?

Stream: general

[Kevin Buzzard]

Should

import tactic

example (P : Prop) : P → P := by {tauto!}

work? (it doesn't; but

example (P : Prop) : P → P := by {tauto! }

does)

[Kenny Lau]

well this doesn't matter because in the current style we always use { xxx } (one space after the opening bracket and one space before the closing bracket)