Mercurial > urweb

diff src/elab_util.sml @ 84:e86370850c30

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Disjointness assumptions
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 12:10:46 -0400
parents b4f2a258e52c
children 1f85890c9846
line wrap: on
line diff
--- a/src/elab_util.sml	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/elab_util.sml	Tue Jul 01 12:10:46 2008 -0400
@@ -124,6 +124,14 @@
                          S.map2 (mfc (bind (ctx, Rel (x, k))) c,
                               fn c' =>
                                  (CAbs (x, k', c'), loc)))
+              | CDisjoint (c1, c2, c3) =>
+                S.bind2 (mfc ctx c1,
+                      fn c1' =>
+                         S.bind2 (mfc ctx c2,
+                              fn c2' =>
+                                 S.map2 (mfc ctx c3,
+                                         fn c3' =>
+                                            (CDisjoint (c1', c2', c3'), loc))))
 
               | CName _ => S.return2 cAll