From b1e720e6cc2b0b96e9df5d99307fab052ec6ce76 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 15 Oct 2020 15:40:56 -0700
Subject: [PATCH] chore: use `#lang lean4` instead of `new_frontend`

---
 src/Lean/Elab/PreDefinition/Basic.lean        | 3 ++-
 src/Lean/Elab/PreDefinition/Main.lean         | 2 +-
 src/Lean/Elab/PreDefinition/MkInhabitant.lean | 2 +-
 src/Lean/Elab/PreDefinition/Structural.lean   | 2 +-
 src/Lean/Elab/PreDefinition/WF.lean           | 2 +-
 src/Lean/Elab/Tactic/Basic.lean               | 2 +-
 src/Lean/Elab/Tactic/Binders.lean             | 2 +-
 src/Lean/Elab/Tactic/ElabTerm.lean            | 2 +-
 src/Lean/Elab/Tactic/Generalize.lean          | 2 +-
 src/Lean/Elab/Tactic/Induction.lean           | 2 +-
 src/Lean/Elab/Tactic/Injection.lean           | 2 +-
 src/Lean/Elab/Tactic/Location.lean            | 2 +-
 src/Lean/Elab/Tactic/Match.lean               | 2 +-
 src/Lean/Elab/Tactic/Rewrite.lean             | 2 +-
 14 files changed, 15 insertions(+), 14 deletions(-)

diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean
index ddb2e4a7aa..24e9c93005 100644
--- a/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Basic.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -8,7 +9,7 @@ import Lean.Meta.AbstractNestedProofs
 import Lean.Elab.Term
 import Lean.Elab.DefView
 import Lean.Elab.PreDefinition.MkInhabitant
-new_frontend
+
 namespace Lean.Elab
 open Meta
 open Term
diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index 3f1a4ec1c5..1bc146ef29 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -6,7 +7,6 @@ Authors: Leonardo de Moura
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural
 import Lean.Elab.PreDefinition.WF
-new_frontend
 namespace Lean.Elab
 open Meta
 open Term
diff --git a/src/Lean/Elab/PreDefinition/MkInhabitant.lean b/src/Lean/Elab/PreDefinition/MkInhabitant.lean
index 0355111873..efcfb5c346 100644
--- a/src/Lean/Elab/PreDefinition/MkInhabitant.lean
+++ b/src/Lean/Elab/PreDefinition/MkInhabitant.lean
@@ -1,10 +1,10 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Meta.AppBuilder
-new_frontend
 namespace Lean.Elab
 open Meta
 
diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean
index 37953cf12c..a9fe679a7c 100644
--- a/src/Lean/Elab/PreDefinition/Structural.lean
+++ b/src/Lean/Elab/PreDefinition/Structural.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -8,7 +9,6 @@ import Lean.Meta.ForEachExpr
 import Lean.Meta.RecursorInfo
 import Lean.Meta.Match.Match
 import Lean.Elab.PreDefinition.Basic
-new_frontend
 namespace Lean.Elab
 open Meta
 
diff --git a/src/Lean/Elab/PreDefinition/WF.lean b/src/Lean/Elab/PreDefinition/WF.lean
index 9720fdb961..c511659a8b 100644
--- a/src/Lean/Elab/PreDefinition/WF.lean
+++ b/src/Lean/Elab/PreDefinition/WF.lean
@@ -1,10 +1,10 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Elab.PreDefinition.Basic
-new_frontend
 namespace Lean
 namespace Elab
 open Meta
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index a8e7afe846..f0b9e4fb81 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -12,7 +13,6 @@ import Lean.Meta.Tactic.Subst
 import Lean.Elab.Util
 import Lean.Elab.Term
 import Lean.Elab.Binders
-new_frontend
 namespace Lean.Elab
 open Meta
 
diff --git a/src/Lean/Elab/Tactic/Binders.lean b/src/Lean/Elab/Tactic/Binders.lean
index 10a779b6a5..67c60f5e70 100644
--- a/src/Lean/Elab/Tactic/Binders.lean
+++ b/src/Lean/Elab/Tactic/Binders.lean
@@ -1,10 +1,10 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Elab.Tactic.Basic
-new_frontend
 namespace Lean.Elab.Tactic
 
 private def liftTermBinderSyntax : Macro :=
diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index 68193d1803..94783181ed 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -8,7 +9,6 @@ import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Assert
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.SyntheticMVars
-new_frontend
 
 namespace Lean.Elab.Tactic
 open Meta
diff --git a/src/Lean/Elab/Tactic/Generalize.lean b/src/Lean/Elab/Tactic/Generalize.lean
index de79bb1ad2..4269162843 100644
--- a/src/Lean/Elab/Tactic/Generalize.lean
+++ b/src/Lean/Elab/Tactic/Generalize.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -7,7 +8,6 @@ import Lean.Meta.Tactic.Generalize
 import Lean.Meta.Check
 import Lean.Meta.Tactic.Intro
 import Lean.Elab.Tactic.ElabTerm
-new_frontend
 
 namespace Lean.Elab.Tactic
 open Meta
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 05bc249cf3..51fd809dd1 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -9,7 +10,6 @@ import Lean.Meta.Tactic.Induction
 import Lean.Meta.Tactic.Cases
 import Lean.Elab.Tactic.ElabTerm
 import Lean.Elab.Tactic.Generalize
-new_frontend
 
 namespace Lean.Elab.Tactic
 open Meta
diff --git a/src/Lean/Elab/Tactic/Injection.lean b/src/Lean/Elab/Tactic/Injection.lean
index cbf17344a9..06b643666c 100644
--- a/src/Lean/Elab/Tactic/Injection.lean
+++ b/src/Lean/Elab/Tactic/Injection.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -5,7 +6,6 @@ Authors: Leonardo de Moura
 -/
 import Lean.Meta.Tactic.Injection
 import Lean.Elab.Tactic.ElabTerm
-new_frontend
 namespace Lean.Elab.Tactic
 
 -- optional (" with " >> many1 ident')
diff --git a/src/Lean/Elab/Tactic/Location.lean b/src/Lean/Elab/Tactic/Location.lean
index f25437d59e..3648eca3ff 100644
--- a/src/Lean/Elab/Tactic/Location.lean
+++ b/src/Lean/Elab/Tactic/Location.lean
@@ -1,9 +1,9 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-new_frontend
 namespace Lean.Elab.Tactic
 
 inductive Location
diff --git a/src/Lean/Elab/Tactic/Match.lean b/src/Lean/Elab/Tactic/Match.lean
index ea0d5b695c..17d8183e9d 100644
--- a/src/Lean/Elab/Tactic/Match.lean
+++ b/src/Lean/Elab/Tactic/Match.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -6,7 +7,6 @@ Authors: Leonardo de Moura
 import Lean.Elab.Match
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.Induction
-new_frontend
 
 namespace Lean.Elab.Tactic
 
diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean
index a7b6db7a95..4ceb5f89d5 100644
--- a/src/Lean/Elab/Tactic/Rewrite.lean
+++ b/src/Lean/Elab/Tactic/Rewrite.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -8,7 +9,6 @@ import Lean.Meta.Tactic.Replace
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.ElabTerm
 import Lean.Elab.Tactic.Location
-new_frontend
 namespace Lean.Elab.Tactic
 open Meta