aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.ml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2014-05-09 11:59:24 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2014-05-09 11:59:24 +0200
commitb1c0584f24cb3732e1704a85452f4fe535e50f33 (patch)
tree1e5285441beb5567c44cda5ee99ec4fd9a6ac140 /pretyping/evarconv.ml
parenta8ee1bef887fbf14ffe1380152993b0db4298c98 (diff)
Restore implicit arguments of irreflexivity (fixes bug #3305).
Diffstat (limited to 'pretyping/evarconv.ml')
0 files changed, 0 insertions, 0 deletions