@@ -1720,9 +1720,10 @@ runTactical fc env tm = do tm' <- eval tm
1720 rty = foldr mkPi res args
1720 rty = foldr mkPi res args
1721 (checked, ty') <- lift $ check ctxt [] rty
1721 (checked, ty') <- lift $ check ctxt [] rty
1722 case normaliseAll ctxt [] (finalise ty') of
1722 case normaliseAll ctxt [] (finalise ty') of
1723+ UType _ -> return ()
1724+ TType _ -> return ()
1723− TType _ -> lift . tfail . InternalMsg $
1725+ ty'' -> lift . tfail . InternalMsg $
1724− show checked ++ " is not a type: it's " ++ show ty'
1726+ show checked ++ " is not a type: it's " ++ show ty''
1726 case lookupDefExact n ctxt of
1727 case lookupDefExact n ctxt of
1727 Just _ -> lift . tfail . InternalMsg $
1728 Just _ -> lift . tfail . InternalMsg $
1728 show n ++ " is already defined."
1729 show n ++ " is already defined."