From f5d03e25a2b13453e0079bef07f148c45bfeced5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 6 Mar 2019 12:03:24 +0100
Subject: [PATCH] be more explicit about quantification order

---
 theories/base_logic/lib/gen_heap.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 494844854..8268ee417 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -81,7 +81,7 @@ Proof.
 Qed.
 
 Section gen_heap.
-  Context `{Countable L, !gen_heapG L V Σ}.
+  Context {L V} `{Countable L, !gen_heapG L V Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : V → iProp Σ.
   Implicit Types σ : gmap L V.
-- 
GitLab