aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/metasyntax.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2017-08-24 00:04:11 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2017-08-24 00:04:11 +0200
commit7b1ff0c70a3ba9cd3cfa5aa6723f8f8a2b6e5396 (patch)
tree9b2fec8fda79a39b4321dee60ed9a9dd18fd66e6 /vernac/metasyntax.ml
parent325890a83a2b073d9654b5615c585cd65a376fbd (diff)
Update .mailmap file.
Diffstat (limited to 'vernac/metasyntax.ml')
0 files changed, 0 insertions, 0 deletions