diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index 7ef86fa5bf6b2884e98731fb1f79cf11d2bbab24..a8967b34e0be6d9563fe6f9f470372854b12de9d 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -279,6 +279,8 @@ Section proofmode_classes.
   Context `{!irisGS Λ Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : val Λ → iProp Σ.
+  Implicit Types v : val Λ.
+  Implicit Types e : expr Λ.
 
   Global Instance frame_twp p s E e R Φ Ψ :
     (∀ v, Frame p R (Φ v) (Ψ v)) →
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index bb54d99620522901afaf95a321b1396f3b35724c..f3856a38870ce223cf35c750551933123106b54c 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -361,6 +361,8 @@ Section proofmode_classes.
   Context `{!irisGS Λ Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : val Λ → iProp Σ.
+  Implicit Types v : val Λ.
+  Implicit Types e : expr Λ.
 
   Global Instance frame_wp p s E e R Φ Ψ :
     (∀ v, Frame p R (Φ v) (Ψ v)) →