From 1f160c6b7cd4b5df6ab37ac5c86e4d74ce72b1fb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 29 Aug 2016 22:31:49 +0200
Subject: [PATCH] Make gmap_empty Opaque to avoid simpl unfolding it.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This happened for example in <[i:=x]>∅, where simpl unfold insert (despite
it being declared simpl never) because ∅ reduces to a constructor.
---
 theories/gmap.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/gmap.v b/theories/gmap.v
index 88f62e36..ca240f3d 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -33,6 +33,7 @@ Defined.
 Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) := λ i m,
   let (m,_) := m in m !! encode i.
 Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap ∅ I.
+Global Opaque gmap_empty.
 Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A → option A) m i :
   gmap_wf m → gmap_wf (partial_alter f (encode i) m).
 Proof.
-- 
GitLab