Coq allows in its grammar the use of the keyword Remark as an _assertionkeyword in the same context as Theorem, Definition, and the like, with its specific semantics: http://coq.inria.fr/refman/Reference-Manual003.html#Vernacular. I happen to use it sometimes but it's not part of the CoqThm syntax group in syntax/coq.vim. I propose to add it with this patch.
osa1
commented
10 years ago
Coq allows in its grammar the use of the keyword Remark as an _assertionkeyword in the same context as Theorem, Definition, and the like, with its specific semantics: http://coq.inria.fr/refman/Reference-Manual003.html#Vernacular. I happen to use it sometimes but it's not part of the CoqThm syntax group in syntax/coq.vim. I propose to add it with this patch.