From cdaf74c3be05efdf43a81741383d81e951f8ba56 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 7 Jan 2021 12:45:19 +0100
Subject: [PATCH] Use `Implicit Types` in HeapLang tests; this fixes
 compilation with Coq 8.11.

---
 tests/heap_lang.ref | 2 +-
 tests/heap_lang.v   | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index b17918505..784aad7a5 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -195,7 +195,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   Σ : gFunctors
   heapG0 : heapG Σ
   E1, E2 : coPset
-  P : iPropI Σ
+  P : iProp Σ
   ============================
   Atomic (stuckness_to_atomicity NotStuck) (#() #())
 
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 5196629e5..2401114aa 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -325,6 +325,7 @@ End inv_mapsto_tests.
 
 Section atomic.
   Context `{!heapG Σ}.
+  Implicit Types P Q : iProp Σ.
 
   (* These tests check if a side-condition for [Atomic] is generated *)
   Check "wp_iMod_fupd_atomic".
-- 
GitLab