From 7865cb372d95c42542d59cbcf83ba541b0ab3f8a Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Tue, 24 Feb 2009 12:01:24 -0500
Subject: Switch to TDisjoint from CDisjoint; still need to implement
 obligation generation at EDisjoint uses

---
 src/elab.sml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'src/elab.sml')

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
-- 
cgit v1.2.3