@@ -28,8 +28,7 @@ data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
2828
2929-- | A list of available tactics and their argument requirements
3030tacticArgs :: [(String, Maybe TacticArg)]
31−tacticArgs = [ ("intro", Nothing)
32− , ("intros", Nothing)
31+tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)
3332 , ("refine", Just ExprTArg)
3433 , ("mrefine", Just ExprTArg)
3534 , ("rewrite", Just ExprTArg)
@@ -41,7 +40,7 @@ tacticArgs = [ ("intro", Nothing)
4140 , ("fill", Just ExprTArg)
4241 , ("try", Just AltsTArg)
4342 ] ++ map (\x -> (x, Nothing)) [
44− "intro", "intros", "compute", "trivial", "solve", "attack",
43+ "intros", "compute", "trivial", "solve", "attack",
4544 "state", "term", "undo", "qed", "abandon", ":q"
4645 ]
4746tactics = map fst tacticArgs