@@ -247,7 +247,7 @@ ProofExpr ::=
247247-}
248248proofExpr :: SyntaxInfo -> IdrisParser PTerm
249249proofExpr syn = do reserved "proof"
250− ts <- indentedBlock (tactic syn)
250+ ts <- indentedBlock1 (tactic syn)
251251 return $ PProof ts
252252 <?> "proof block"
253253
@@ -260,7 +260,7 @@ TacticsExpr :=
260260-}
261261tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
262262tacticsExpr syn = do reserved "tactics"
263− ts <- indentedBlock (tactic syn)
263+ ts <- indentedBlock1 (tactic syn)
264264 return $ PTactics ts
265265 <?> "tactics block"
266266