diff lib/ur/incl.ur @ 1181:618f9f458da9

Got split1 working, but noticed a nasty type inference bug with transplanted unification variables
author Adam Chlipala <adamc@hcoop.net>
date Sat, 06 Mar 2010 19:14:48 -0500
parents ac3dbbc85c6e
children 0b1d666bddb4
line wrap: on
line diff
--- a/lib/ur/incl.ur	Sat Mar 06 16:15:26 2010 -0500
+++ b/lib/ur/incl.ur	Sat Mar 06 19:14:48 2010 -0500
@@ -21,7 +21,7 @@
     i [f nm t r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') =>
                       i'.Hide [f nm t] (f [nm] [t] [r ++ r''] !))
 
-fun inv2 [K] [nm :: Name] [t ::: K] [r :: {K}] [r' :: {K}] [[nm] ~ r]
+fun inv2 [K] [nm :: Name] [t :: K] [r :: {K}] [r' :: {K}] [[nm] ~ r]
          (i : incl ([nm = t] ++ r) r') =
     i [incl r r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') =>
                       fn [tp :: Type] (f : r''' :: {K} -> [r ~ r'''] => incl' r r' r''' -> tp) =>
@@ -35,6 +35,6 @@
     (i : tf []) (fl : folder r) =
     @Top.fold [fn r' => incl r' r -> tf r']
      (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] acc i =>
-         f [nm] [v] [r'] ! i (acc (inv2 [nm] [r'] [r] i)))
+         f [nm] [v] [r'] ! i (acc (inv2 [nm] [v] [r'] [r] i)))
      (fn _ => i)
      fl (incl [r] [[]])