diff options
Diffstat (limited to 'src/elab_env.sig')
| -rw-r--r-- | src/elab_env.sig | 20 |
1 files changed, 15 insertions, 5 deletions
diff --git a/src/elab_env.sig b/src/elab_env.sig index c4e5ae5a..f24206ee 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -34,17 +34,27 @@ signature ELAB_ENV = sig exception UnboundRel of int exception UnboundNamed of int + datatype 'a var = + NotBound + | Rel of int * 'a + | Named of int * 'a + val pushCRel : env -> string -> Elab.kind -> env val lookupCRel : env -> int -> string * Elab.kind val pushCNamed : env -> string -> Elab.kind -> env * int val pushCNamedAs : env -> string -> int -> Elab.kind -> env val lookupCNamed : env -> int -> string * Elab.kind + + val lookupC : env -> string -> Elab.kind var + + val pushERel : env -> string -> Elab.con -> env + val lookupERel : env -> int -> string * Elab.con + + val pushENamed : env -> string -> Elab.con -> env * int + val pushENamedAs : env -> string -> int -> Elab.con -> env + val lookupENamed : env -> int -> string * Elab.con - datatype var = - CNotBound - | CRel of int * Elab.kind - | CNamed of int * Elab.kind - val lookupC : env -> string -> var + val lookupE : env -> string -> Elab.con var end |