diff --git a/Tactic.agda b/Tactic.agda
index 8b45b658..8cbdd207 100644
--- a/Tactic.agda
+++ b/Tactic.agda
@@ -14,6 +14,7 @@ open import Tactic.Constrs public
 open import Tactic.EquationalReasoning public
 open import Tactic.Eta public
 open import Tactic.Intro public
+open import Tactic.J public
 open import Tactic.ReduceDec public
 
 open import Tactic.Derive.DecEq public
diff --git a/Tactic/J.agda b/Tactic/J.agda
index 174be9a6..d8c4cebe 100644
--- a/Tactic/J.agda
+++ b/Tactic/J.agda
@@ -7,11 +7,11 @@
 -- via `open import Tactic.J (quote J) (quote refl)`
 --------------------------------------------------------------------------------
 
-open import Meta
+open import Meta.Init
 
 module Tactic.J (J-name refl-name : Name) where
 
-open import Meta.Prelude
+open import Meta.Prelude hiding (J)
 
 open import Class.Monad
 open import Class.MonadError
@@ -46,14 +46,13 @@ macro
 
 private
   module Test where
-    open import Relation.Binary.PropositionalEquality
+    open import Relation.Binary.PropositionalEquality hiding (J)
     open ≡-Reasoning
     open import Tactic.Defaults
 
     -- since we can't use names abstractly, we need to do some yoga here
 
     private variable
-      A : Set
       x y z w : A
 
     J : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {x : A} (P : (y : A) → x ≡ y → Set ℓ₂)