diff --git a/theories/mapset.v b/theories/mapset.v
index fe0d2c7bae1645bd285b586ee7a76a1f90e55e53..184839d831ca695ff844613edb2b0f8d8d0ce762 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.