aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/coqrst/notations/TacticNotationsVisitor.py
AgeCommit message (Expand)Author
2019-05-16[refman] Introduce syntax for alternatives in notationsClément Pit-Claudel
2018-03-12[Sphinx] Add a few grammar constructionsMaxime Dénès
2018-03-09Integration of a sphinx-based documentation generator.Maxime Dénès