Mercurial > urweb
comparison 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 |
comparison
equal
deleted
inserted
replaced
1268:236dc296c32d | 1269:9f4b9315810d |
---|---|
698 | (L'.CRel n1, L'.CRel n2) => n1 <> n2 | 698 | (L'.CRel n1, L'.CRel n2) => n1 <> n2 |
699 | (L'.CRel _, L'.CNamed _) => true | 699 | (L'.CRel _, L'.CNamed _) => true |
700 | (L'.CNamed _, L'.CRel _) => true | 700 | (L'.CNamed _, L'.CRel _) => true |
701 | (L'.CRel _, L'.CModProj _) => true | 701 | (L'.CRel _, L'.CModProj _) => true |
702 | (L'.CModProj _, L'.CRel _) => true | 702 | (L'.CModProj _, L'.CRel _) => true |
703 | (L'.CModProj (_, _, n1), L'.CModProj (_, _, n2)) => n1 <> n2 | |
703 | _ => false | 704 | _ => false |
704 | 705 |
705 and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) = | 706 and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) = |
706 let | 707 let |
707 (*val () = eprefaces "Summaries" [("loc", PD.string (ErrorMsg.spanToString loc)), | 708 (*val () = eprefaces "Summaries" [("loc", PD.string (ErrorMsg.spanToString loc)), |