aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/omega
diff options
context:
space:
mode:
authorGravatar Amin Timany <amintimany@gmail.com>2017-05-27 09:44:38 +0200
committerGravatar Amin Timany <amintimany@gmail.com>2017-05-28 22:29:12 +0200
commitbde0f3038bffa660b0fc15084fb99bce42c7aa43 (patch)
treee198656fe5f7ec9d5df2a5043c069ae958d5d4f3 /plugins/omega
parent1c74df16e7a539f21418ddb09419ff0106960789 (diff)
Fix a bug in checker
Universe constraints of the inductive types were not instantiated before being pushed on the environment. This commit fixes this bug.
Diffstat (limited to 'plugins/omega')
0 files changed, 0 insertions, 0 deletions