@@ -1,3 +1,4 @@
1+
12{-# LANGUAGE PatternGuards #-}
23module Idris.Prover (prover, showProof, showRunElab) where
34
@@ -89,7 +90,10 @@ prove mode opt ctxt lit n ty
8990 (tm, prf) <-
9091 if mode
9192 then elabloop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) [] Nothing []
92− else ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing
93+ else do iputStrLn $ "Warning: this interactive prover is deprecated and will be removed " ++
94+ "in a future release. Please see :elab for a similar feature that "++
95+ "will replace it."
96+ ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing
9397 logLvl 1 $ "Adding " ++ show tm
9498 i <- getIState
9599 let shower = if mode