From d77b159c8d5275caf05e31a192dfcdaf257b2de2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 4 Dec 2020 18:15:27 +0100
Subject: [PATCH] fix build for Coq 8.10

---
 iris_heap_lang/proofmode.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 3f8c07228..f2441bbaa 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -58,10 +58,10 @@ Lemma tac_twp_value_nofupd `{!heapG Σ} Δ s E Φ v :
   envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
 Proof. rewrite envs_entails_eq=> ->. by apply twp_value. Qed.
 
-Lemma tac_wp_value `{!heapG Σ} Δ s E Φ v :
+Lemma tac_wp_value `{!heapG Σ} Δ s E (Φ : val → iPropI Σ) v :
   envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
 Proof. rewrite envs_entails_eq=> ->. by rewrite wp_value_fupd. Qed.
-Lemma tac_twp_value `{!heapG Σ} Δ s E Φ v :
+Lemma tac_twp_value `{!heapG Σ} Δ s E (Φ : val → iPropI Σ) v :
   envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
 Proof. rewrite envs_entails_eq=> ->. by rewrite twp_value_fupd. Qed.
 
-- 
GitLab