From 276b6129962c7ed8d742b70e9f941db0ebd8a5fa Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Thu, 26 Jun 2008 09:03:38 -0400
Subject: Proper subsignaturing for sub-signatures

---
 src/elaborate.sml | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

(limited to 'src/elaborate.sml')

diff --git a/src/elaborate.sml b/src/elaborate.sml
index d2d468db..b4d13f0c 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1353,9 +1353,18 @@ fun subSgn env sgn1 (sgn2 as (_, loc2)) =
                                  case sgi1 of
                                      L'.SgiSgn (x', n1, sgn1) =>
                                      if x = x' then
-                                         (subSgn env sgn1 sgn2;
-                                          subSgn env sgn2 sgn1;
-                                          SOME env)
+                                         let
+                                             val () = subSgn env sgn1 sgn2
+                                             val () = subSgn env sgn2 sgn1
+
+                                             val env = E.pushSgnNamedAs env x n2 sgn2
+                                             val env = if n1 = n2 then
+                                                           env
+                                                       else
+                                                           E.pushSgnNamedAs env x n1 sgn2
+                                         in
+                                             SOME env
+                                         end
                                      else
                                          NONE
                                    | _ => NONE)
-- 
cgit v1.2.3