From cb1daa491531ee88195764560a76c1cd31fbde1d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 25 May 2021 11:18:28 +0200
Subject: [PATCH] Revert "Make `mapset_elem_of` Opaque."

This reverts commit 267cc7086dd684d4e536f8898ccdefe34dd7c80e.

Thanks to @jung for spotting this was a NOP, see https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/263#note_67379
---
 theories/mapset.v | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/theories/mapset.v b/theories/mapset.v
index fe0d2c7b..184839d8 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -132,8 +132,4 @@ 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.
-
 Global Arguments mapset_eq_dec : simpl never.
-- 
GitLab