From d28cad7cc5881018717c7e875c99c51469da9d44 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Tue, 1 Jul 2008 11:39:14 -0400
Subject: Threading disjointness conditions through Elaborate

---
 src/disjoint.sml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'src/disjoint.sml')

diff --git a/src/disjoint.sml b/src/disjoint.sml
index 784bd635..fa4c8618 100644
--- a/src/disjoint.sml
+++ b/src/disjoint.sml
@@ -277,10 +277,7 @@ fun prove env denv (c1, c2, loc) =
         val hasUnknown = List.exists (fn p => p = Unknown)
     in
         if hasUnknown ps1 orelse hasUnknown ps2 then
-            (ErrorMsg.errorAt loc "Structure of row is too complicated to prove disjointness";
-             Print.eprefaces' [("Row 1", ElabPrint.p_con env c1),
-                               ("Row 2", ElabPrint.p_con env c2)];
-             [])
+            [(c1, c2)]
         else
             foldl (fn (p1, rem) =>
                       foldl (fn (p2, rem) =>
-- 
cgit v1.2.3