diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-05 09:43:30 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-05 09:43:30 +0200 |
| commit | 38a749767b74c1fc67d02948efd13ea8c5cbcd0b (patch) | |
| tree | 2573c6767ff2cf0268a2862b637b83a99558fa01 /vernac/topfmt.mli | |
| parent | 734d152ae1faf5feb427b978badc6ed0c95f4d5f (diff) | |
| parent | 66b1132128481b0e3a461862518e9eaf34838e0c (diff) | |
Merge PR #850: Improve grammar in RefMan-Gal and RefMan-syn
Diffstat (limited to 'vernac/topfmt.mli')
0 files changed, 0 insertions, 0 deletions