aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/locality.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-17 09:06:09 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-17 09:06:09 +0100
commitac3ee8cba2d27f2be38ba706e49aeee08086d936 (patch)
tree67c2633ac657abd1b5bc2a26b27b7cb7a9aad868 /vernac/locality.ml
parentf2bbdd31a6aa62d8a000f5a91f666e68e7241964 (diff)
parent105f346cc707b3433379514cd5ddcd3389912083 (diff)
Merge PR#437: Improve unification debug trace.
Diffstat (limited to 'vernac/locality.ml')
0 files changed, 0 insertions, 0 deletions