diff options
| author | Clément Pit-Claudel | 2018-04-29 23:15:48 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2018-05-15 12:05:44 -0400 |
| commit | efa6ef592e29bb4bc862a114c399d660580bba66 (patch) | |
| tree | 86bf3720805ea3b7ea218b9d5fb7a6b27a20a883 /dev/tools | |
| parent | 8cc98698e8fc2cf86c5173c2dc0834538a2ca075 (diff) | |
[doc] Document all directives and roles of our Sphinx domain
Also get rid of a few unused or redundant constructs: the :ltac: role and the
'tac' directive (unused) and the :gallina: and :notation: roles (redundant).
Diffstat (limited to 'dev/tools')
0 files changed, 0 insertions, 0 deletions