summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-11-05 11:33:59 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-11-05 11:33:59 -0400
commit16901075111d5bb14fa583b50dc64579008962aa (patch)
treee43b5aa8730132eb49cb35a2ca2cc919379c0d5d
parentfe997cad0b4ba41c1fcd2f6ba9bb2402afecf72e (diff)
Strengthen consNeq, to avoid unwise unifications
-rw-r--r--src/elaborate.sml4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index a80f11d0..5ba4df42 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -773,6 +773,10 @@
| (L'.CRel _, L'.CModProj _) => true
| (L'.CModProj _, L'.CRel _) => true
| (L'.CModProj (_, _, n1), L'.CModProj (_, _, n2)) => n1 <> n2
+ | (L'.CModProj _, L'.CName _) => true
+ | (L'.CName _, L'.CModProj _) => true
+ | (L'.CNamed _, L'.CName _) => true
+ | (L'.CName _, L'.CNamed _) => true
| _ => false
and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) =