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)),