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