aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-03-04 00:32:58 +0100
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-03-04 00:32:58 +0100
commit85fc5f90c52a755d1b64640f4f0b3421979c0fe8 (patch)
treeaf7c16aa9db83cb81a0994dfab3364cf0d50702b /theories/Structures
parentc35c97e7c904f2109110c64f2ba9e45e945de381 (diff)
Fix bug #3532, providing universe inconsistency information when a
unification fails due to that, during a conversion step.
Diffstat (limited to 'theories/Structures')
0 files changed, 0 insertions, 0 deletions