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