aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-06-01 10:44:57 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-06-01 10:44:57 -0400
commit3c8cef34259e14736ea0847e0e6aa51b40c01ac1 (patch)
tree87387c268342bec1241299f2f1bc3288275bb528 /src/elaborate.sml
parent58a0405bf44a93409be9c31020982b2257625c82 (diff)
Improve consNeq to detect unequal projected cons
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index cda8e8d8..67ed3383 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -700,6 +700,7 @@
| (L'.CNamed _, L'.CRel _) => true
| (L'.CRel _, L'.CModProj _) => true
| (L'.CModProj _, L'.CRel _) => true
+ | (L'.CModProj (_, _, n1), L'.CModProj (_, _, n2)) => n1 <> n2
| _ => false
and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) =