@@ -12,6 +12,7 @@ import Idris.Delaborate
1212import Idris.Compiler
1313import Idris.Prover
1414import Idris.Parser
15+import Idris.Coverage
1516import Paths_idris
1617
1718import Core.Evaluate
@@ -194,7 +195,12 @@ process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
194195 ist <- get
195196 let tm' = specialise ctxt (idris_statics ist) tm
196197 iputStrLn (show (delab ist tm'))
197−process fn (Prove n) = prover (lit fn) n
198+process fn (Prove n) = do prover (lit fn) n
199+ -- recheck totality
200+ i <- get
201+ totcheck (FC "(input)" 0, n)
202+ mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
203+ mapM_ checkDeclTotality (idris_totcheck i)
198204process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t
199205 ctxt <- getContext
200206 ist <- get