chore: delete restate_axiom (#6939)

This isn't used in Mathlib4, and wasn't useful during the port, so I think we can just drop it now. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Sep 4, 2023 · faba1c3 · faba1c3
1 parent 8dea0d0
commit faba1c3
Show file tree

Hide file tree

Showing 7 changed files with 0 additions and 80 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -3104,7 +3104,6 @@ import Mathlib.Tactic.Relation.Trans
 import Mathlib.Tactic.Rename
 import Mathlib.Tactic.RenameBVar
 import Mathlib.Tactic.Replace
-import Mathlib.Tactic.RestateAxiom
 import Mathlib.Tactic.Rewrites
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.Ring.Basic

diff --git a/Mathlib/CategoryTheory/Category/Basic.lean b/Mathlib/CategoryTheory/Category/Basic.lean
@@ -5,7 +5,6 @@ Authors: Stephen Morgan, Scott Morrison, Johannes Hölzl, Reid Barton
 -/
 import Mathlib.CategoryTheory.Category.Init
 import Mathlib.Combinatorics.Quiver.Basic
-import Mathlib.Tactic.RestateAxiom
 import Mathlib.Tactic.PPWithUniv
 
 #align_import category_theory.category.basic from "leanprover-community/mathlib"@"2efd2423f8d25fa57cf7a179f5d8652ab4d0df44"

diff --git a/Mathlib/Mathport/Syntax.lean b/Mathlib/Mathport/Syntax.lean
@@ -72,7 +72,6 @@ import Mathlib.Tactic.Relation.Trans
 import Mathlib.Tactic.Rename
 import Mathlib.Tactic.RenameBVar
 import Mathlib.Tactic.Replace
-import Mathlib.Tactic.RestateAxiom
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.RSuffices
 import Mathlib.Tactic.RunCmd

diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
@@ -126,7 +126,6 @@ import Mathlib.Tactic.Relation.Trans
 import Mathlib.Tactic.Rename
 import Mathlib.Tactic.RenameBVar
 import Mathlib.Tactic.Replace
-import Mathlib.Tactic.RestateAxiom
 import Mathlib.Tactic.Rewrites
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.Ring.Basic

diff --git a/Mathlib/Tactic/RestateAxiom.lean b/Mathlib/Tactic/RestateAxiom.lean
diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt
@@ -119,7 +119,6 @@ Mathlib/Tactic/Recover.lean : line 10 : ERR_MOD : Module docstring missing, or t
 Mathlib/Tactic/Rename.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 Mathlib/Tactic/RenameBVar.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 Mathlib/Tactic/Replace.lean : line 9 : ERR_MOD : Module docstring missing, or too late
-Mathlib/Tactic/RestateAxiom.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 Mathlib/Tactic/Set.lean : line 4 : ERR_AUT : Authors line should look like: 'Authors: Jean Dupont, Иван Иванович Иванов'
 Mathlib/Tactic/Set.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 Mathlib/Tactic/SimpRw.lean : line 9 : ERR_MOD : Module docstring missing, or too late

diff --git a/test/restate_axiom.lean b/test/restate_axiom.lean