adud

Closing a {…} badly jams the prover.

1

Consider the following *erroneous* code: ``` Goal True /\ True. split. 2:{ tauto.} tauto. Qed. ``` There should be a space between `tauto.` and `}`, but instead of returning an...