# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1275403497 14400
# Node ID 9f4b9315810dc564c65252a4d68dd7c3b45b065e
# Parent  236dc296c32d197b1f776add5ba7502e90d42d9a
Improve consNeq to detect unequal projected cons

diff -r 236dc296c32d -r 9f4b9315810d src/elaborate.sml
--- 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) =