aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/declareDef.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-16 22:48:39 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-16 22:48:39 +0200
commit4078547a44619701e9a719876b716877d0368bc4 (patch)
tree47218bcb1d6f0933d75c147caae9879c60b9d16a /vernac/declareDef.ml
parentf0863099fe7b9d29b887edcb6aea12291c56a1dc (diff)
Fix typo in CHANGES.
Diffstat (limited to 'vernac/declareDef.ml')
0 files changed, 0 insertions, 0 deletions