Placate the linter

leanprover-community · Oct 19, 2020 · f0f9895 · f0f9895
1 parent 6e595ec
commit f0f9895
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/tactic/dependencies.lean b/src/tactic/dependencies.lean
@@ -5,8 +5,6 @@ Authors: Jannis Limperg
 -/
 import tactic.core
 
-open native
-
 /-!
 # Tactics About Dependencies
 
@@ -56,6 +54,8 @@ These are the hypotheses that syntactically appear in the hypothesis's type (or
 value, if the hypothesis is a local definition).
 -/
 
+open native
+
 namespace tactic
 
 private meta def local_set_to_name_set (lcs : expr_set) : name_set :=