search

the-lambda-church / coquille

Interactive theorem proving with Coq in vim.
ISC License
186 stars 68 forks source link

Syntax Highlighting error on nested Lemma #40

Closed tbelaire closed 8 years ago

tbelaire commented 8 years ago

The syntax highlighting doesn't properly handle the case of

Lemma foo: 1 = 1.
Proof.
    Lemma L : 2 = 2.
        auto.
    Qed.
    auto.
Qed.

As the second auto. is marked in red as an error.

trefis commented 8 years ago

From the README:

Note that by default, you will be in the pathogen-bundle branch, which also ships Vincent Aravantinos syntax and indent scripts for Coq, as well as an ftdetect script. If you already have those in your vim config, then just switch to the master branch.

Which I like to use as an excuse to not look at highlighting problems.

(The real reason is: I've tried looking at them in the past, but then I had to be locked up for a few weeks. So I try to stay away from vim's syntax files now).

trefis commented 8 years ago

Of course you're more than welcome to send a pull request or to contact the author of these files directly and let us know how it goes.

tbelaire commented 8 years ago

Yeah, I normally try and fix any bugs, but it was in a syntax file, so I tried to punt it your way :P.

I'll just not next lemmas.