diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda
index 3e4627c..9702bf9 100644
--- a/Analysis/Forward.agda
+++ b/Analysis/Forward.agda
@@ -259,7 +259,7 @@ module WithProg (prog : Program) where
     open WithEvaluator
     open WithEvaluator using (result; analyze; result≈analyze-result) public
 
-    private module WithInterpretation {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}} where
+    private module _ {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}} where
         open LatticeInterpretation latticeInterpretationˡ
             using ()
             renaming
@@ -300,8 +300,6 @@ module WithProg (prog : Program) where
             ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs'} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ
                      (inj₂ (⟦⟧ᵛ-foldr ⟦vs⟧ρ vs∈vss'))
 
-    open WithInterpretation
-
     module _ {{evaluator : Evaluator}} {{interpretation : LatticeInterpretation isLatticeˡ}} where
         open Evaluator evaluator
         open LatticeInterpretation interpretation
@@ -314,8 +312,8 @@ module WithProg (prog : Program) where
             {{evaluator}} : Evaluator
             {{interpretation}} : LatticeInterpretation isLatticeˡ
 
-        open Evaluator evaluator
-        open LatticeInterpretation interpretation
+        open Evaluator evaluator public
+        open LatticeInterpretation interpretation public
 
         field
             valid : IsValid