@@ -28,8 +28,8 @@ mkPatTm t = do i <- getIState
28 evalStateT (toTT (mapPT deNS timp)) 0
28 evalStateT (toTT (mapPT deNS timp)) 0
30 toTT (PRef _ n) = do i <- lift getIState
30 toTT (PRef _ n) = do i <- lift getIState
31− case lookupDef n (tt_ctxt i) of
31+ case lookupNameDef n (tt_ctxt i) of
32− [TyDecl nt _] -> return $ P nt n Erased
32+ [(n', TyDecl nt _)] -> return $ P nt n' Erased
33 _ -> return $ P Ref n Erased
33 _ -> return $ P Ref n Erased
34 toTT (PApp _ t args) = do t' <- toTT t
34 toTT (PApp _ t args) = do t' <- toTT t
35 args' <- mapM (toTT . getTm) args
35 args' <- mapM (toTT . getTm) args