refactor(frontends/lean/tactic_notation): remove irtactic in favor of itactic

library/init/meta/async_tactic.lean

@@ -50,7 +50,7 @@ namespace interactive
 open interactive.types
 
 /-- Proves the first goal asynchronously as a separate lemma. -/
-meta def async (tac : irtactic) : tactic unit :=
+meta def async (tac : itactic) : tactic unit :=
 prove_goal_async tac
 
 end interactive

library/init/meta/interactive.lean

@@ -118,7 +118,7 @@ private meta def parser_desc_aux : expr → tactic (list format)
 meta def param_desc : expr → tactic format
 | ```(parse %%p) := join <$> parser_desc_aux p
 | ```(opt_param %%t ._) := (++ "?") <$> pp t
-| e := if is_constant e ∧ (const_name e)^.components^.ilast ∈ [`itactic, `irtactic]
+| e := if is_constant e ∧ (const_name e)^.components^.ilast = `itactic
   then return $ to_fmt "{ tactic }"
   else paren <$> pp e
 end interactive
@@ -147,15 +147,6 @@ itactic: parse a nested "interactive" tactic. That is, parse
 meta def itactic : Type :=
 tactic unit
 
-/-
-irtactic: parse a nested "interactive" tactic. That is, parse
-  `{` tactic `}`
-It is similar to itactic, but the interactive mode will report errors
-when any of the nested tactics fail. This is good for tactics such as async and abstract.
--/
-meta def irtactic : Type :=
-tactic unit
-
 /--
 This tactic applies to a goal that is either a Pi/forall or starts with a let binder.
 
@@ -382,7 +373,7 @@ tactic.try
 meta def solve1 : itactic → tactic unit :=
 tactic.solve1
 
-meta def abstract (id : parse ident? ) (tac : irtactic) : tactic unit :=
+meta def abstract (id : parse ident? ) (tac : itactic) : tactic unit :=
 tactic.abstract tac id
 
 meta def all_goals : itactic → tactic unit :=
@@ -391,7 +382,7 @@ tactic.all_goals
 meta def any_goals : itactic → tactic unit :=
 tactic.any_goals
 
-meta def focus (tac : irtactic) : tactic unit :=
+meta def focus (tac : itactic) : tactic unit :=
 tactic.focus [tac]
 
 /--

library/init/meta/smt/interactive.lean

@@ -40,9 +40,6 @@ local postfix *:9001 := many
 meta def itactic : Type :=
 smt_tactic unit
 
-meta def irtactic : Type :=
-smt_tactic unit
-
 meta def intros : parse ident* → smt_tactic unit
 | [] := smt_tactic.intros
 | hs := smt_tactic.intro_lst hs

src/frontends/lean/tactic_notation.cpp

@@ -148,7 +148,6 @@ static expr parse_interactive_tactic(parser & p, name const & decl_name, name co
     auto pos = p.pos();
     expr type     = p.env().get(decl_name).get_type();
     name itactic  = get_interactive_tactic_full_name(tac_class, "itactic");
-    name irtactic = get_interactive_tactic_full_name(tac_class, "irtactic");
     buffer<expr> args;
     try {
         try {
@@ -164,8 +163,6 @@ static expr parse_interactive_tactic(parser & p, name const & decl_name, name co
                         args.push_back(parse_interactive_param(p, arg_args[0], arg_args[1], arg_args[2]));
                     } else if (is_constant(arg_type, itactic)) {
                         args.push_back(parse_nested_interactive_tactic(p, tac_class, use_istep));
-                    } else if (is_constant(arg_type, irtactic)) {
-                        args.push_back(parse_nested_interactive_tactic(p, tac_class, use_istep));
                     } else {
                         break;
                     }

tests/lean/interactive/focus.lean.expected.out

@@ -1,4 +1,4 @@
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"record":{"source":,"state":"a b c : ℕ,\na_1 : a = b,\na_2 : b = 0\n⊢ a = 0","tactic_param_idx":0,"tactic_params":["{ tactic }"],"text":"focus","type":"tactic.interactive.irtactic → tactic unit"},"response":"ok","seq_num":5}
-{"record":{"source":,"state":"b c : ℕ,\na_2 : b = 0\n⊢ b = 0","tactic_param_idx":0,"tactic_params":["{ tactic }"],"text":"focus","type":"tactic.interactive.irtactic → tactic unit"},"response":"ok","seq_num":7}
+{"record":{"source":,"state":"a b c : ℕ,\na_1 : a = b,\na_2 : b = 0\n⊢ a = 0","tactic_param_idx":0,"tactic_params":["{ tactic }"],"text":"focus","type":"tactic.interactive.itactic → tactic unit"},"response":"ok","seq_num":5}
+{"record":{"source":,"state":"b c : ℕ,\na_2 : b = 0\n⊢ b = 0","tactic_param_idx":0,"tactic_params":["{ tactic }"],"text":"focus","type":"tactic.interactive.itactic → tactic unit"},"response":"ok","seq_num":7}
 {"record":{"state":"b c : ℕ,\na_2 : b = 0\n⊢ b = 0\n\na b c : ℕ,\na_1 : a = b,\na_2 : b = 0\n⊢ b = a"},"response":"ok","seq_num":9}