Merge remote-tracking branch 'upstream/master'
commit147352c99f39825febaa2434007200b52afb9666
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateTue 17 Mar 2015, 11:11 (12 years ago)
parentbf8dbc9cfbb866
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