Mercurial > urweb

diff src/elab_util.sml @ 85:1f85890c9846

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Disjointness assumptions in expressions
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 12:25:12 -0400
parents e86370850c30
children 7bab29834cd6
line wrap: on
line diff
--- a/src/elab_util.sml	Tue Jul 01 12:10:46 2008 -0400
+++ b/src/elab_util.sml	Tue Jul 01 12:25:12 2008 -0400
@@ -104,6 +104,14 @@
                          S.map2 (mfc (bind (ctx, Rel (x, k))) c,
                               fn c' =>
                                  (TCFun (e, x, k', c'), loc)))
+              | TDisjoint (c1, c2, c3) =>
+                S.bind2 (mfc ctx c1,
+                      fn c1' =>
+                         S.bind2 (mfc ctx c2,
+                              fn c2' =>
+                                 S.map2 (mfc ctx c3,
+                                         fn c3' =>
+                                            (TDisjoint (c1', c2', c3'), loc))))
               | TRecord c =>
                 S.map2 (mfc ctx c,
                         fn c' =>