From b9104d069ebbe96d3cc84b5e2e39f759fdca16d2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Sep 2020 14:28:12 -0700
Subject: [PATCH] chore: adjust code

---
 src/Lean/Elab/Tactic/Basic.lean | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 4e13299ee6..41221fcb73 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -246,6 +246,15 @@ modifyMCtx fun mctx =>
 @[builtinTactic seq] def evalSeq : Tactic :=
 fun stx => (stx.getArg 0).forSepArgsM evalTactic
 
+@[builtinTactic paren] def evalParen : Tactic :=
+fun stx => evalTactic (stx.getArg 1)
+
+@[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic :=
+fun stx => withRef (stx.getArg 2) $ focus $ (stx.getArg 1).forSepArgsM evalTactic
+
+@[builtinTactic tacticSeq] def evalTacticSeq : Tactic :=
+fun stx => evalTactic (stx.getArg 0)
+
 partial def evalChoiceAux (tactics : Array Syntax) : Nat → TacticM Unit
 | i =>
   if h : i < tactics.size then
@@ -376,12 +385,6 @@ fun stx => match_syntax stx with
   | `(tactic| subst $hs*) => forEachVar hs Meta.subst
   | _                     => throwUnsupportedSyntax
 
-@[builtinTactic paren] def evalParen : Tactic :=
-fun stx => evalTactic (stx.getArg 1)
-
-@[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic :=
-fun stx => withRef (stx.getArg 2) $ focus $ (stx.getArg 1).forSepArgsM evalTactic
-
 /--
   First method searches for a metavariable `g` s.t. `tag` is a suffix of its name.
   If none is found, then it searches for a metavariable `g` s.t. `tag` is a prefix of its name. -/