@@ -1850,6 +1850,7 @@ runTac autoSolve ist perhapsFC fn tac
1850 Just fc ->
1850 Just fc ->
1851 do fill $ reflectFC fc
1851 do fill $ reflectFC fc
1853+ runT Qed = lift . tfail $ Msg "The qed command is only valid in the interactive prover"
1853 runT x = fail $ "Not implemented " ++ show x
1854 runT x = fail $ "Not implemented " ++ show x
1855 runReflected t = do t' <- reify ist t
1856 runReflected t = do t' <- reify ist t