Merge pull request #2006 from david-christiansen/issue/1790
Better error message for qed in expressions
commitcfbb866f0c9edd77f2bd6ad0891f72b1e02a9f71
authorDavid Christiansen <david@davidchristiansen.dk>
dateTue 17 Mar 2015, 10:05 (12 years ago)
parent39ba43215ab5d5
src/Idris/ElabTerm.hs+1
@@ -1850,6 +1850,7 @@ runTac autoSolve ist perhapsFC fn tac
18501850 Just fc ->
18511851 do fill $ reflectFC fc
18521852 solve
1853+ runT Qed = lift . tfail $ Msg "The qed command is only valid in the interactive prover"
18531854 runT x = fail $ "Not implemented " ++ show x
18541855
18551856 runReflected t = do t' <- reify ist t