diff src/elab_util.sml @ 207:cc68da3801bc

Non-star SELECT
author Adam Chlipala <adamc@hcoop.net>
date Thu, 14 Aug 2008 18:35:08 -0400
parents cb8f69556975
children e86411f647c6
line wrap: on
line diff
--- a/src/elab_util.sml	Thu Aug 14 15:27:35 2008 -0400
+++ b/src/elab_util.sml	Thu Aug 14 18:35:08 2008 -0400
@@ -68,6 +68,11 @@
 
               | KUnit => S.return2 kAll
 
+              | KTuple ks =>
+                S.map2 (ListUtil.mapfold mfk ks,
+                        fn ks' =>
+                           (KTuple ks', loc))
+
               | KError => S.return2 kAll
 
               | KUnif (_, _, ref (SOME k)) => mfk' k
@@ -180,6 +185,16 @@
 
               | CUnit => S.return2 cAll
 
+              | CTuple cs =>
+                S.map2 (ListUtil.mapfold (mfc ctx) cs,
+                        fn cs' =>
+                           (CTuple cs', loc))
+
+              | CProj (c, n) =>
+                S.map2 (mfc ctx c,
+                        fn c' =>
+                           (CProj (c', n), loc))
+
               | CError => S.return2 cAll
               | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c
               | CUnif _ => S.return2 cAll