aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/obligations.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-16 09:40:24 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-16 09:40:24 +0200
commit96d53d99d32f7006e553c6772b9c983925fb31f6 (patch)
tree2f205484417bda6fd7d59397015ef4080d7d964b /vernac/obligations.ml
parent75b69fd5bb32e89b565551b96ca8d02d2d16ae62 (diff)
parent00745dd8a0a9597c7f3eecab7578d7069f85386a (diff)
Merge PR #948: [doc] Write (@nil nat) instead of (nil nat)
Diffstat (limited to 'vernac/obligations.ml')
0 files changed, 0 insertions, 0 deletions