@@ -161,8 +161,16 @@ reifyTTApp t [t', Constant (I i)]
161161 return $ Proj t'' i
162162reifyTTApp t [tt]
163163 | t == reflm "TType" = liftM TType (reifyTTUExp tt)
164+reifyTTApp t [tt]
165+ | t == reflm "UType" = liftM UType (reifyUniverse tt)
164166reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))
165167
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)
173+
166174-- | Reify raw terms from their reflected representation
167175reifyRaw :: Term -> ElabD Raw
168176reifyRaw t@(App _ _ _)