@@ -161,8 +161,16 @@ reifyTTApp t [t', Constant (I i)]
161 return $ Proj t'' i
161 return $ Proj t'' i
162reifyTTApp t [tt]
162reifyTTApp t [tt]
163 | t == reflm "TType" = liftM TType (reifyTTUExp tt)
163 | t == reflm "TType" = liftM TType (reifyTTUExp tt)
165+ | t == reflm "UType" = liftM UType (reifyUniverse tt)
164reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))
166reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))
168+reifyUniverse :: Term -> ElabD Universe
169+reifyUniverse (P _ n _) | n == reflm "AllTypes" = return AllTypes
170+ | n == reflm "UniqueType" = return UniqueType
171+ | n == reflm "NullType" = return NullType
172+reifyUniverse tm = fail ("Unknown reflection universe: " ++ show tm)
166-- | Reify raw terms from their reflected representation
174-- | Reify raw terms from their reflected representation
167reifyRaw :: Term -> ElabD Raw
175reifyRaw :: Term -> ElabD Raw
168reifyRaw t@(App _ _ _)
176reifyRaw t@(App _ _ _)