From d0993d07a12381b227ea218d7031380f48b151c3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 6 Sep 2020 08:40:48 -0700 Subject: [PATCH] chore: rename `Definition.lean` => `DefView.lean` --- src/Lean/Elab/Declaration.lean | 2 +- src/Lean/Elab/{Definition.lean => DefView.lean} | 0 src/Lean/Elab/Inductive.lean | 2 +- src/Lean/Elab/MutualDef.lean | 2 +- 4 files changed, 3 insertions(+), 3 deletions(-) rename src/Lean/Elab/{Definition.lean => DefView.lean} (100%) diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index 0e50b1b933..c6d15e7baa 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich -/ import Lean.Util.CollectLevelParams import Lean.Elab.DeclUtil -import Lean.Elab.Definition +import Lean.Elab.DefView import Lean.Elab.Inductive import Lean.Elab.Structure import Lean.Elab.MutualDef diff --git a/src/Lean/Elab/Definition.lean b/src/Lean/Elab/DefView.lean similarity index 100% rename from src/Lean/Elab/Definition.lean rename to src/Lean/Elab/DefView.lean diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index c4fe858110..6d56e899d9 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -9,7 +9,7 @@ import Lean.Util.CollectLevelParams import Lean.Util.Constructions import Lean.Elab.Command import Lean.Elab.CollectFVars -import Lean.Elab.Definition +import Lean.Elab.DefView import Lean.Elab.DeclUtil namespace Lean diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 261db49e29..aa51e31688 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura import Lean.Meta.Closure import Lean.Meta.Check import Lean.Elab.Command -import Lean.Elab.Definition +import Lean.Elab.DefView namespace Lean namespace Elab