Switch to TDisjoint from CDisjoint; still need to implement obligation generation at EDisjoint uses

1 files changed, 1 insertions, 5 deletions

diff --git a/src/elab.sml b/src/elab.sml
index 9ec3793e..3fed1918 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -49,21 +49,17 @@ datatype explicitness =
          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