From 3c8cef34259e14736ea0847e0e6aa51b40c01ac1 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Tue, 1 Jun 2010 10:44:57 -0400
Subject: Improve consNeq to detect unequal projected cons

---
 src/elaborate.sml | 1 +
 1 file changed, 1 insertion(+)

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) =
-- 
cgit v1.2.3