Mercurial > urweb

diff lib/ur/incl.ur @ 1182:0b1d666bddb4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
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)) =