diff options
author | 2017-08-16 09:40:24 +0200 | |
---|---|---|
committer | 2017-08-16 09:40:24 +0200 | |
commit | 96d53d99d32f7006e553c6772b9c983925fb31f6 (patch) | |
tree | 2f205484417bda6fd7d59397015ef4080d7d964b /plugins/ltac/g_class.ml4 | |
parent | 75b69fd5bb32e89b565551b96ca8d02d2d16ae62 (diff) | |
parent | 00745dd8a0a9597c7f3eecab7578d7069f85386a (diff) |
Merge PR #948: [doc] Write (@nil nat) instead of (nil nat)
Diffstat (limited to 'plugins/ltac/g_class.ml4')
0 files changed, 0 insertions, 0 deletions