@@ -28,8 +28,7 @@ data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
29-- | A list of available tactics and their argument requirements
29-- | A list of available tactics and their argument requirements
30tacticArgs :: [(String, Maybe TacticArg)]
30tacticArgs :: [(String, Maybe TacticArg)]
31−tacticArgs = [ ("intro", Nothing)
31+tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)
32− , ("intros", Nothing)
33 , ("refine", Just ExprTArg)
32 , ("refine", Just ExprTArg)
34 , ("mrefine", Just ExprTArg)
33 , ("mrefine", Just ExprTArg)
35 , ("rewrite", Just ExprTArg)
34 , ("rewrite", Just ExprTArg)
@@ -41,7 +40,7 @@ tacticArgs = [ ("intro", Nothing)
41 , ("fill", Just ExprTArg)
40 , ("fill", Just ExprTArg)
42 , ("try", Just AltsTArg)
41 , ("try", Just AltsTArg)
43 ] ++ map (\x -> (x, Nothing)) [
42 ] ++ map (\x -> (x, Nothing)) [
44− "intro", "intros", "compute", "trivial", "solve", "attack",
43+ "intros", "compute", "trivial", "solve", "attack",
45 "state", "term", "undo", "qed", "abandon", ":q"
44 "state", "term", "undo", "qed", "abandon", ":q"
47tactics = map fst tacticArgs
46tactics = map fst tacticArgs