@@ -1928,11 +1928,15 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
19281928 = do solve
19291929 returnUnit
19301930 | n == tacN "prim__Goal", [] <- args
1931− = do (h:_) <- get_holes
1932− t <- goal
1933− fmap fst . checkClosed $
1934− rawPair (Var (reflm "TTName"), Var (reflm "TT"))
1935− (reflectName h, reflect t)
1931+ = do hs <- get_holes
1932+ case hs of
1933+ (h : _) -> do t <- goal
1934+ fmap fst . checkClosed $
1935+ rawPair (Var (reflm "TTName"), Var (reflm "TT"))
1936+ (reflectName h, reflect t)
1937+ [] -> lift . tfail . Msg $
1938+ "Elaboration is complete. There are no goals."
1939+
19361940 | n == tacN "prim__Holes", [] <- args
19371941 = do hs <- get_holes
19381942 fmap fst . checkClosed $