diff --git a/lib/Core/Common.ml b/lib/Core/Common.ml
index 3544cd5..92d9948 100644
--- a/lib/Core/Common.ml
+++ b/lib/Core/Common.ml
@@ -1,6 +1,6 @@
 (* number ; is-hole? *)
-type meta = Mv of int * bool
-
+type meta
+  = Mv of int * bool
 
 let cMV : int ref = ref 0
 
diff --git a/lib/Core/Eval.ml b/lib/Core/Eval.ml
index 36d1a55..b916e7d 100644
--- a/lib/Core/Eval.ml
+++ b/lib/Core/Eval.ml
@@ -1,15 +1,13 @@
 module V = Value
 module T = Term
+module M = Metaenv
 
-let rec index (env : V.env) (i : int) = 
-  match env with
-  | []      -> failwith "Can't happen"
-  | x :: xs -> if i < 1 then x else index xs (i-1)
+open List
 
 let rec eval (env : V.env) (tr : T.term) =
   match tr with
-  | Var  (Ix i)               -> index env i
-  | Mv   m                    -> V.Stuck (V.Meta m, ?)
+  | Var  (Ix i)               -> nth env i
+  | Meta (Mv (i, b))          -> V.Stuck (V.Meta (Mv (i, b)), M.getMetaType i)
   | Type                      -> V.Type
   | T0                        -> V.T0
   | Ind0 (B b, t)             -> begin
diff --git a/lib/Core/Metaenv.ml b/lib/Core/Metaenv.ml
new file mode 100644
index 0000000..d303d7c
--- /dev/null
+++ b/lib/Core/Metaenv.ml
@@ -0,0 +1,13 @@
+module C = Common
+module V = Value
+
+open List
+
+type mentry = {m: C.meta; ty: V.value}
+
+let metaEntries : mentry list ref = ref []
+
+let getMetaEntry (i : int) =
+  nth (! metaEntries) i
+
+let getMetaType (i : int) = (getMetaEntry i).ty
diff --git a/lib/Raw/PostProcess.ml b/lib/Raw/PostProcess.ml
index 3592458..9beeba3 100644
--- a/lib/Raw/PostProcess.ml
+++ b/lib/Raw/PostProcess.ml
@@ -1,6 +1,5 @@
 module P = AbsImplicitt
 module R = RawSyntax
-module C = Common
 
 open R
 
@@ -34,17 +33,18 @@ let rec proc (e : P.id list) (ex : P.exp) =
   | ExpPair (e1, e2) -> Pair (proc e e1, proc e e2)
   | ExpFst e1 -> Fst (proc e e1)
   | ExpSnd e1 -> Snd (proc e e1)
-  | ExpHole -> C.Mv (getCMV (), true)
-  | ExpInd0 (Id i1, e1, e2) -> Ind0 (B (proc (i1 :: e)) e1) e2
-  | ExpIndN (Id i1, e1, e2, Id i2, Id i3, e3, e4) ->
-     IndN (B (proc (i1 :: e) e1)) (proc e e2)
-       (B (B (proc (i3 :: i2 :: e) e3)))
-       (proc e e4)
-  | ExpIndB (Id i1, e1, e2, e3, e4) ->
-     IndB (B (proc (i1 :: e) e1))
-       (proc e e2)
-       (proc e e3)
-       (proc e e4)
+  | ExpHole -> Hole
+  | ExpInd0 (i1, e1, e2) -> Ind0 (proc (i1 :: e) e1, proc e e2)
+  | ExpIndN (i1, e1, e2, i2, i3, e3, e4) ->
+     IndN (proc (i1 :: e) e1
+         , proc e e2
+         , proc (i3 :: i2 :: e) e3
+         , proc e e4)
+  | ExpIndB (i1, e1, e2, e3, e4) ->
+     IndB (proc (i1 :: e) e1
+         , proc e e2
+         , proc e e3
+         , proc e e4)
 
 and unwrapLambda (e : P.id list) (bs : P.bD list) (sc : P.exp) =
   match bs with
diff --git a/lib/Raw/RawSyntax.ml b/lib/Raw/RawSyntax.ml
index 9bef074..e7d5591 100644
--- a/lib/Raw/RawSyntax.ml
+++ b/lib/Raw/RawSyntax.ml
@@ -1,3 +1,5 @@
+module C = Core.Common
+
 type var = Ix of int
 type name = string
 
@@ -7,6 +9,7 @@ type icit
 
 type ast
   = Var of var
+  | Hole
 
   | Type