summaryrefslogtreecommitdiff
path: root/src/elab_env.sig
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-01-26 17:26:14 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-01-26 17:26:14 -0500
commit1469fd94659b3562ea7e3c180e0366194717a287 (patch)
tree6a9e3d51ca7418b53b04aa4cbfbc9f779f2747fa /src/elab_env.sig
parentc3c7a475626786988f0a367fc3c20f903f3fcbba (diff)
Added simple expression constructors to Elab
Diffstat (limited to 'src/elab_env.sig')
-rw-r--r--src/elab_env.sig20
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