aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-09-23 17:31:40 +0200
committerPierre-Marie Pédrot2018-09-23 17:33:00 +0200
commita3cbf400d291fe0427f28d2847a0002cb17474dc (patch)
tree4a105a3bcda5b67731ae722babeedf83a2ba41f6 /kernel
parent92fbd7383c3897b3932b0ad95afa0982d2d8a7e3 (diff)
Fix #8513: EConstr.eq_constr doesn't properly take into account universe variables.
We simply normalize the universe variables before comparing them.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions