search

xavierleroy / coq2html

An HTML documentation generator for Coq source files
GNU General Public License v2.0
30 stars 11 forks source link

Add support for the Variant coq keyword #6

Closed ddemange closed 4 years ago

ddemange commented 4 years ago

It would be nice to have the Variant keyword recognized, and highlighted as the Inductive keyword in the output html. Currently, this doesn't seem to be the case. The fix may be as simple as adding it to the coq_keywords set.

xavierleroy commented 4 years ago

Sure. Commit 466627c updates the lists of keywords and tactics, including Variant.

ddemange commented 4 years ago

Great, thanks!