aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/mltop.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-19 11:44:46 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-19 11:44:46 +0200
commit9933871efd122163f7e2dfe8377b9b2dd384b47b (patch)
treecd348cb40e310a9a2003a085e8c7707448789649 /vernac/mltop.ml
parent7e4535d62c4f8abc6537206e7abc34f1bb0be69d (diff)
parent7760c6d58ca35b97b0893dc4911ab22c9a5a49ec (diff)
Merge PR #1036: Unify EConstr.t equality
Diffstat (limited to 'vernac/mltop.ml')
0 files changed, 0 insertions, 0 deletions