-
Guillaume Melquiond authored
Discard old pieces between Qed and the next blank line, so that generated commands about implicit arguments are not preserved.
ee535a72
Discard old pieces between Qed and the next blank line, so that generated commands about implicit arguments are not preserved.