aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/record.mli
diff options
context:
space:
mode:
authorGravatar Amin Timany <amintimany@gmail.com>2017-04-26 15:24:35 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-16 04:51:16 +0200
commit7b5fcef8a0fb3b97a3980f10596137234061990f (patch)
tree41512a4619f9b68641cb9da31b56059846e8a0b9 /vernac/record.mli
parent40f56eb0f79e208fc4b1b4ed2f0fb49c69c13a2f (diff)
Fix bugs
Diffstat (limited to 'vernac/record.mli')
0 files changed, 0 insertions, 0 deletions