Mercurial > urweb
comparison src/elab_env.sig @ 13:6049e2193bf2
Lifting cons in ElabEnv
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 08 Jun 2008 11:32:48 -0400 |
parents | e97c6d335869 |
children | f1c36df29ed7 |
comparison
equal
deleted
inserted
replaced
12:d89477f07c1e | 13:6049e2193bf2 |
---|---|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE | 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE |
25 * POSSIBILITY OF SUCH DAMAGE. | 25 * POSSIBILITY OF SUCH DAMAGE. |
26 *) | 26 *) |
27 | 27 |
28 signature ELAB_ENV = sig | 28 signature ELAB_ENV = sig |
29 | |
30 exception SynUnif | |
31 val liftConInCon : int -> Elab.con -> Elab.con | |
29 | 32 |
30 type env | 33 type env |
31 | 34 |
32 val empty : env | 35 val empty : env |
33 | 36 |
55 val pushENamedAs : env -> string -> int -> Elab.con -> env | 58 val pushENamedAs : env -> string -> int -> Elab.con -> env |
56 val lookupENamed : env -> int -> string * Elab.con | 59 val lookupENamed : env -> int -> string * Elab.con |
57 | 60 |
58 val lookupE : env -> string -> Elab.con var | 61 val lookupE : env -> string -> Elab.con var |
59 | 62 |
63 val declBinds : env -> Elab.decl -> env | |
64 | |
60 end | 65 end |