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