diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-12-20 00:42:45 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-20 00:42:45 +0100 |
commit | 4902ec974dcce7c4f7b5cdca413f67395b649214 (patch) | |
tree | 78915833016b02b6e0a03f700d0d1fdad584bf39 /vernac/vernacprop.ml | |
parent | b3b3798fca7fd05f31cb921f981c15ee81507b0d (diff) | |
parent | b1352aff5c8e22d200a3e161538d2a5b8adb4c13 (diff) |
Merge PR #6470: Fix typo in the refman.
Diffstat (limited to 'vernac/vernacprop.ml')
0 files changed, 0 insertions, 0 deletions