# HG changeset patch # User Adam Chlipala # Date 1320507239 14400 # Node ID fb0388f1180e5b5ebf202fc3742ad9e73f004004 # Parent 65d6488c82d53293290bc20b9511e7ee4b80bdb8 Strengthen consNeq, to avoid unwise unifications diff -r 65d6488c82d5 -r fb0388f1180e src/elaborate.sml --- a/src/elaborate.sml Sat Nov 05 09:56:52 2011 -0400 +++ b/src/elaborate.sml Sat Nov 05 11:33:59 2011 -0400 @@ -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) =