From 267cc7086dd684d4e536f8898ccdefe34dd7c80e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 15 Mar 2019 11:13:34 +0100
Subject: [PATCH] Make `mapset_elem_of` Opaque.

Hopefully this fixes https://gitlab.mpi-sws.org/iris/iris/issues/232
---
 theories/mapset.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/mapset.v b/theories/mapset.v
index 7481faad..20529a20 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -130,4 +130,8 @@ Proof.
 Qed.
 End mapset.
 
+(** [mapset_elem_of] internally contains an equality; make sure that tactics do
+not unfold it and try to unify [∈] against goals with [=]. *)
+Opaque mapset_elem_of.
+
 Arguments mapset_eq_dec : simpl never.
-- 
GitLab