whonore / Coqtail

Interactive Coq Proofs in Vim
MIT License
274 stars 34 forks source link

Transparency hints are highlighted in red #285

Closed Tuplanolla closed 2 years ago

Tuplanolla commented 2 years ago

Versions

Coq 8.15.0

Coqtail 1.6.2

Vim 8.2

Equations 1.3

Python 3.7.4

Description

In the following commands, both occurrences of Typeclasses are highlighted in red, suggesting that they are syntax errors, even though they are really not.

#[export] Typeclasses Opaque iff.
#[export] Typeclasses Transparent is_true.