diff options
author | 2018-06-21 19:07:29 +0200 | |
---|---|---|
committer | 2018-06-21 19:07:29 +0200 | |
commit | 01fcf80e83ff85bf07cd3dc59cadad096b68ac92 (patch) | |
tree | 031de4d062639137eb2e98e67c7463b672792a33 /vernac/g_vernac.ml4 | |
parent | 4a3697da7be172c1559588d326a2f02c80bb98e9 (diff) | |
parent | 7f528cdb0ee42a40792d242357a239969f51cada (diff) |
Merge PR #7770: Move indices on top on the TOC. Closes #7764.
Diffstat (limited to 'vernac/g_vernac.ml4')
0 files changed, 0 insertions, 0 deletions