diff src/elaborate.sml @ 1269:9f4b9315810d

Improve consNeq to detect unequal projected cons
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jun 2010 10:44:57 -0400
parents 79b2bcac6200
children 9fd0cb0ef6e1
line wrap: on
line diff
--- a/src/elaborate.sml	Sun May 30 10:39:25 2010 -0400
+++ b/src/elaborate.sml	Tue Jun 01 10:44:57 2010 -0400
@@ -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) =