diff --git a/library/init/meta/interactive_base.lean b/library/init/meta/interactive_base.lean
index ed07a1916a..411e539761 100644
--- a/library/init/meta/interactive_base.lean
+++ b/library/init/meta/interactive_base.lean
@@ -110,6 +110,7 @@ private meta def parser_desc_aux : expr → tactic (list format)
 | `(pure ._) := return []
 | `(._ <$> %%p) := parser_desc_aux p
 | `(skip_info %%p) := parser_desc_aux p
+| `(._ <$ %%p) := parser_desc_aux p
 | `(set_goal_info_pos %%p) := parser_desc_aux p
 | `(with_desc %%desc %%p) := list.ret <$> eval_expr format desc
 | `(%%p₁ <*> %%p₂) := do
@@ -124,6 +125,10 @@ private meta def parser_desc_aux : expr → tactic (list format)
   f₁ ← parser_desc_aux p₁,
   f₂ ← parser_desc_aux p₂,
   return $ concat f₁ f₂
+| `(%%p₁ >> %%p₂) := do
+  f₁ ← parser_desc_aux p₁,
+  f₂ ← parser_desc_aux p₂,
+  return $ concat f₁ f₂
 | `(many %%p) := do
   f ← parser_desc_aux p,
   return [maybe_paren f ++ "*"]