diff src/elab.sml @ 334:9601c717d2f3

queryX
author Adam Chlipala <adamc@hcoop.net>
date Sat, 13 Sep 2008 19:49:53 -0400
parents 42dfb0d61cf0
children e976b187d73a
line wrap: on
line diff
--- a/src/elab.sml	Sat Sep 13 14:58:57 2008 -0400
+++ b/src/elab.sml	Sat Sep 13 19:49:53 2008 -0400
@@ -46,10 +46,14 @@
          Explicit
        | Implicit
 
+datatype auto_instantiate =
+         Instantiate
+       | LeaveAlone
+
 datatype con' =
          TFun of con * con
        | TCFun of explicitness * string * kind * con
-       | TDisjoint of con * con * con
+       | TDisjoint of auto_instantiate * con * con * con
        | TRecord of con
 
        | CRel of int