Mercurial > urweb
comparison src/elab_env.sig @ 623:588b9d16b00a
Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 22 Feb 2009 16:10:25 -0500 |
parents | 33d5bd69da00 |
children | 7292bcb7c02d |
comparison
equal
deleted
inserted
replaced
622:d64533157f40 | 623:588b9d16b00a |
---|---|
44 | 44 |
45 datatype 'a var = | 45 datatype 'a var = |
46 NotBound | 46 NotBound |
47 | Rel of int * 'a | 47 | Rel of int * 'a |
48 | Named of int * 'a | 48 | Named of int * 'a |
49 | |
50 val pushKRel : env -> string -> env | |
51 val lookupKRel : env -> int -> string | |
52 val lookupK : env -> string -> int option | |
49 | 53 |
50 val pushCRel : env -> string -> Elab.kind -> env | 54 val pushCRel : env -> string -> Elab.kind -> env |
51 val lookupCRel : env -> int -> string * Elab.kind | 55 val lookupCRel : env -> int -> string * Elab.kind |
52 | 56 |
53 val pushCNamed : env -> string -> Elab.kind -> Elab.con option -> env * int | 57 val pushCNamed : env -> string -> Elab.kind -> Elab.con option -> env * int |