# HG changeset patch # User Adam Chlipala # Date 1268175042 18000 # Node ID 0b1d666bddb48dbd9fdb103e8c75b3f714074ea2 # Parent 618f9f458da9de407ec49b250840899bf3737b43 Spiffed-up Split1; remove spurious error message triggered by 'open'ing a module containing a functor diff -r 618f9f458da9 -r 0b1d666bddb4 lib/ur/incl.ur --- a/lib/ur/incl.ur Sat Mar 06 19:14:48 2010 -0500 +++ b/lib/ur/incl.ur Tue Mar 09 17:50:42 2010 -0500 @@ -14,7 +14,7 @@ i [$r1] (fn [r' :: {Type}] [r1 ~ r'] (i' : incl' r1 r2 r') => i'.Expose [fn r => $r] r --- r') -fun inv1 [K] [nm :: Name] [t ::: K] [r :: {K}] [r' :: {K}] [[nm] ~ r] +fun inv1 [K] [nm :: Name] [t :: K] [r :: {K}] [r' :: {K}] [[nm] ~ r] [f :: Name -> K -> {K} -> Type] (i : incl ([nm = t] ++ r) r') (f : nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r)) = diff -r 618f9f458da9 -r 0b1d666bddb4 lib/ur/incl.urs --- a/lib/ur/incl.urs Sat Mar 06 19:14:48 2010 -0500 +++ b/lib/ur/incl.urs Tue Mar 09 17:50:42 2010 -0500 @@ -3,7 +3,7 @@ val incl : K --> r1 :: {K} -> r2 :: {K} -> [r1 ~ r2] => incl r1 (r1 ++ r2) val proj : r1 ::: {Type} -> r2 ::: {Type} -> incl r1 r2 -> $r2 -> $r1 -val inv1 : K --> nm :: Name -> t ::: K -> r :: {K} -> r' :: {K} +val inv1 : K --> nm :: Name -> t :: K -> r :: {K} -> r' :: {K} -> [[nm] ~ r] => f :: (Name -> K -> {K} -> Type) -> incl ([nm = t] ++ r) r' diff -r 618f9f458da9 -r 0b1d666bddb4 lib/ur/mem.ur --- a/lib/ur/mem.ur Sat Mar 06 19:14:48 2010 -0500 +++ b/lib/ur/mem.ur Tue Mar 09 17:50:42 2010 -0500 @@ -34,5 +34,5 @@ (i : tf []) (fl : folder r) = @@Incl.fold [tf] [r] (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] (i : Incl.incl ([nm = v] ++ r') r) acc => - f [nm] [v] [r'] ! (Incl.inv1 [nm] [r'] [r] [mem] i mem) acc) + f [nm] [v] [r'] ! (Incl.inv1 [nm] [v] [r'] [r] [mem] i mem) acc) i fl diff -r 618f9f458da9 -r 0b1d666bddb4 src/elaborate.sml --- a/src/elaborate.sml Sat Mar 06 19:14:48 2010 -0500 +++ b/src/elaborate.sml Tue Mar 09 17:50:42 2010 -0500 @@ -2066,11 +2066,7 @@ fun collect first (st, sgn) = case E.projectConstraints env {sgn = sgn, str = st} of - NONE => (if first then - strError env (UnboundStr (loc, str)) - else - (); - []) + NONE => [] | SOME cs => case #1 (hnormSgn env sgn) of L'.SgnConst sgis =>