aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/coqrst/notations/TacticNotationsLexer.py
AgeCommit message (Collapse)Author
2020-11-09Add additional escape sequences for notationsJim Fehrle
2019-12-19Support additional escape sequences in notationsJim Fehrle
2019-05-16[refman] Introduce syntax for alternatives in notationsClément Pit-Claudel
Closes GH-8482.
2018-04-14[Sphinx] Add chapter 9.Théo Zimmermann
Chapter ported by Théo Zimmermann and Maxime Dénès.
2018-04-09[Sphinx] Make it possible to espace { by %{ in custom grammarsMaxime Dénès
2018-03-12[Sphinx] Add a few grammar constructionsMaxime Dénès
Code from Paul Steckler (MIT).
2018-03-09Integration of a sphinx-based documentation generator.Maxime Dénès
The original contribution is from Clément Pit-Claudel. I updated his code and integrated it with the Coq build system. Many improvements by Paul Steckler (MIT). This commit adds the infrastructure but no content.