Mercurial > urweb
changeset 1182:0b1d666bddb4
Spiffed-up Split1; remove spurious error message triggered by 'open'ing a module containing a functor
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 09 Mar 2010 17:50:42 -0500 |
| parents | 618f9f458da9 |
| children | 9d3ccb8b39ac |
| files | lib/ur/incl.ur lib/ur/incl.urs lib/ur/mem.ur src/elaborate.sml |
| diffstat | 4 files changed, 4 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- 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)) =
--- 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'
--- 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
--- 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 =>