Mercurial > urweb

diff src/elab.sml @ 628:12b73f3c108e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Switch to TDisjoint from CDisjoint; still need to implement obligation generation at EDisjoint uses
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 12:01:24 -0500
parents 588b9d16b00a
children 70cbdcf5989b
line wrap: on
line diff
--- a/src/elab.sml	Sun Feb 22 17:39:55 2009 -0500
+++ b/src/elab.sml	Tue Feb 24 12:01:24 2009 -0500
@@ -49,21 +49,17 @@
          Explicit
        | Implicit
 
-datatype auto_instantiate =
-         Instantiate
-       | LeaveAlone
-
 datatype con' =
          TFun of con * con
        | TCFun of explicitness * string * kind * con
        | TRecord of con
+       | TDisjoint of con * con * con
 
        | CRel of int
        | CNamed of int
        | CModProj of int * string list * string
        | CApp of con * con
        | CAbs of string * kind * con
-       | CDisjoint of auto_instantiate * con * con * con
 
        | CKAbs of string * con
        | CKApp of con * kind