From 788f8eef79f61c8df42c45b50f4f5435fd3d120f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 17 Jun 2021 15:14:55 +0200
Subject: [PATCH] some more implicit types

---
 iris/program_logic/total_weakestpre.v | 2 ++
 iris/program_logic/weakestpre.v       | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index 7ef86fa5b..a8967b34e 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 bb54d9962..f3856a388 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)) →
-- 
GitLab