Mercurial > urweb

diff src/elaborate.sml @ 327:3a57f3b3a3f8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix bug in subsignature check for con synonyms
author Adam Chlipala <adamc@hcoop.net>
date Thu, 11 Sep 2008 18:36:20 -0400
parents 950320f33232
children 58f1260f293f
line wrap: on
line diff
--- 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 ()