diff options
| author | Théo Zimmermann | 2018-07-21 11:51:17 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-07-21 11:51:17 +0200 |
| commit | 106c5b87a36df3b77442ed4784381082e4cc3924 (patch) | |
| tree | ce2329acdbb3c16f64e16a0c592bfab535aa6b3a /dev/include | |
| parent | c56110635536a63117127be8ad07aaff0dc26a0a (diff) | |
A few Sphinx fixes in the Ltac chapter.
Including using subscripts more often.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions