aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/g_vernac.ml4
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-21 17:40:13 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-21 17:40:13 +0200
commit41cf6afdb70b073838bd2a1e71f76c600e03c006 (patch)
treeac599113aa91feef19fa1d59feeaa27a685ce360 /vernac/g_vernac.ml4
parentbe6f66e3d4424b0dfbbbe3097a617aebb8aefca2 (diff)
parent3d8342c2c26f710583e6b9246bd1069cb8b42d7d (diff)
Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter.
Diffstat (limited to 'vernac/g_vernac.ml4')
0 files changed, 0 insertions, 0 deletions