@@ -1,3 +1,4 @@
1{-# LANGUAGE PatternGuards #-}
2{-# LANGUAGE PatternGuards #-}
2module Idris.Prover (prover, showProof, showRunElab) where
3module Idris.Prover (prover, showProof, showRunElab) where
@@ -89,7 +90,10 @@ prove mode opt ctxt lit n ty
89 (tm, prf) <-
90 (tm, prf) <-
91 then elabloop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) [] Nothing []
92 then elabloop 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 "++
92− else ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing
96+ ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing
93 logLvl 1 $ "Adding " ++ show tm
97 logLvl 1 $ "Adding " ++ show tm
94 i <- getIState
98 i <- getIState
95 let shower = if mode
99 let shower = if mode