Sometimes when I edit a proof, I can accidentally cause functions defined with the program tactic to get new obligations. It's hard to find those dangling obligations, because Coq allows new theorems to get started. To combat that problem, I add this after the last obligation:
Fail Next Obligation.
Unfortunately, that breaks syntax highlighting in Coqtail. See how Module ListExample, Definition, Theorem, Proof, and End ListExample are incorrectly highlighted.
Sometimes when I edit a proof, I can accidentally cause functions defined with the program tactic to get new obligations. It's hard to find those dangling obligations, because Coq allows new theorems to get started. To combat that problem, I add this after the last obligation:
Unfortunately, that breaks syntax highlighting in Coqtail. See how
Module ListExample,Definition,Theorem,Proof, andEnd ListExampleare incorrectly highlighted.