search

Ailrun / coq-commenter

Coq commenter for Emacs
GNU General Public License v3.0
6 stars 2 forks source link

[Feature Request] Parse better #4

Closed alxest closed 7 years ago

alxest commented 7 years ago

I use a module named "TODOProof", and when I use definition from there, (e.g. TODOProof.abcd) coq-commenter recognizes this as a proof.

Simply checking that no other alphabet is in front of "Proof" keyword should be sufficient me.

Ailrun commented 7 years ago

Oh.... I missed that case. I will fix this ASAP. (Or, in the other words, when I can use my emacs development environment)

Ailrun commented 7 years ago

@alxest I fix this. At least I believe so.

Please update coq-commenter after its melpa version is updated.