# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1221172580 14400
# Node ID 3a57f3b3a3f8de6550b73da951b0116da191c65d
# Parent  950320f3323250f6c5dfc3a8e99e7e4f950854d1
Fix bug in subsignature check for con synonyms

diff -r 950320f33232 -r 3a57f3b3a3f8 src/elaborate.sml
--- a/src/elaborate.sml	Thu Sep 11 18:32:41 2008 -0400
+++ b/src/elaborate.sml	Thu Sep 11 18:36:20 2008 -0400
@@ -2478,7 +2478,16 @@
                                      fun found (x', n1, k1, c1) =
                                          if x = x' then
                                              let
-                                                 fun good () = SOME (E.pushCNamedAs env x n2 k2 (SOME c2), denv)
+                                                 fun good () =
+                                                     let
+                                                         val env = E.pushCNamedAs env x n2 k2 (SOME c2)
+                                                         val env = if n1 = n2 then
+                                                                       env
+                                                                   else
+                                                                       E.pushCNamedAs env x n1 k1 (SOME c1)
+                                                     in
+                                                         SOME (env, denv)
+                                                     end
                                              in
                                                  (case unifyCons (env, denv) c1 c2 of
                                                       [] => good ()
diff -r 950320f33232 -r 3a57f3b3a3f8 tests/crud.ur
--- a/tests/crud.ur	Thu Sep 11 18:32:41 2008 -0400
+++ b/tests/crud.ur	Thu Sep 11 18:36:20 2008 -0400
@@ -7,7 +7,7 @@
 
         val title : string
 
-        val cols : $(Top.mapTT (fn t => {Show : t -> xbody}) cols)
+        val cols : colMeta cols
 end) = struct
 
 open constraints M
@@ -22,7 +22,7 @@
                                 {fold [fn cols :: {Type} => $cols -> colMeta cols -> xtr]
                                         (fn (nm :: Name) (t :: Type) (rest :: {Type}) acc =>
                                                 [[nm] ~ rest] =>
-                                                fn (r : $([nm = t] ++ rest)) cols =>
+                                                fn r cols =>
                                                 <tr>
                                                         <td>{cols.nm.Show r.nm}</td>
                                                         {acc (r -- nm) (cols -- nm)}