Mercurial > urweb

comparison 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
comparison
equal deleted inserted replaced
627:f4f2b09a533a 628:12b73f3c108e
47 47
48 datatype explicitness = 48 datatype explicitness =
49 Explicit 49 Explicit
50 | Implicit 50 | Implicit
51 51
52 datatype auto_instantiate =
53 Instantiate
54 | LeaveAlone
55
56 datatype con' = 52 datatype con' =
57 TFun of con * con 53 TFun of con * con
58 | TCFun of explicitness * string * kind * con 54 | TCFun of explicitness * string * kind * con
59 | TRecord of con 55 | TRecord of con
56 | TDisjoint of con * con * con
60 57
61 | CRel of int 58 | CRel of int
62 | CNamed of int 59 | CNamed of int
63 | CModProj of int * string list * string 60 | CModProj of int * string list * string
64 | CApp of con * con 61 | CApp of con * con
65 | CAbs of string * kind * con 62 | CAbs of string * kind * con
66 | CDisjoint of auto_instantiate * con * con * con
67 63
68 | CKAbs of string * con 64 | CKAbs of string * con
69 | CKApp of con * kind 65 | CKApp of con * kind
70 | TKFun of string * con 66 | TKFun of string * con
71 67