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