Coqtail icon indicating copy to clipboard operation
Coqtail copied to clipboard
verified publisher icon whonore

Proof `term` breaks highlighting and indenting

Open whonore opened this issue 6 years ago • 1 comments

Proofs of the form

Goal True.
Proof I.

confuse the highlighting and indenting because they expect a Qed.

whonore avatar Jun 13 '19 03:06 whonore

See also https://github.com/coq/coq/pull/827#issuecomment-333349523

andres-erbsen-sifive avatar Jun 19 '19 18:06 andres-erbsen-sifive