From 76dddf93774d125f34d251815fdbb6d4fd9b7f9d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 18 Feb 2015 17:39:19 +0100
Subject: [PATCH] prevent masks from clobbering the == notation

---
 iris_meta.v      |  4 ++--
 iris_vs.v        |  2 +-
 lib/ModuRes/RA.v | 17 +++++++----------
 masks.v          | 11 ++++++++++-
 4 files changed, 20 insertions(+), 14 deletions(-)

diff --git a/iris_meta.v b/iris_meta.v
index ea4bf5dd7..1e7d09779 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -155,7 +155,7 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG).
     Next Obligation.
       intros x y H_xy P m r. simpl in H_xy. destruct n.
       - intros LEZ. exfalso. omega.
-      - intros _. simpl. assert(H_xy': equiv x y) by assumption. rewrite H_xy'. tauto.
+      - intros _. simpl. assert(H_xy': x == y) by assumption. rewrite H_xy'. tauto.
     Qed.
 
       
@@ -217,7 +217,7 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG).
     Next Obligation.
       intros x y H_xy P m r. simpl in H_xy. destruct n.
       - intros LEZ. exfalso. omega.
-      - intros _. simpl. assert(H_xy': equiv x y) by assumption. rewrite H_xy'. tauto.
+      - intros _. simpl. assert(H_xy': x == y) by assumption. rewrite H_xy'. tauto.
     Qed.
 
     Program Definition plugExpr safe m φ P Q: expr -n> Props :=
diff --git a/iris_vs.v b/iris_vs.v
index 28698618f..e2aa64da7 100644
--- a/iris_vs.v
+++ b/iris_vs.v
@@ -168,7 +168,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
         rewrite ->HSub in HP; specialize (HSub i); rewrite HLu in HSub.
         destruct (w' i) as [Ï€' |]; [| contradiction].
         split; [intuition now eauto | intros].
-        simpl in HLw, HSub. change (equiv rri ri0) in HLrs. rewrite <- HLw, <- HSub.
+        simpl in HLw, HSub. change (rri == ri0) in HLrs. rewrite <- HLw, <- HSub.
         apply HInv; [now auto with arith |].
         eapply uni_pred, HP; [now auto with arith |].
         rewrite <-HLrs. clear dependent ri0.
diff --git a/lib/ModuRes/RA.v b/lib/ModuRes/RA.v
index 2e2997354..9c4e14498 100644
--- a/lib/ModuRes/RA.v
+++ b/lib/ModuRes/RA.v
@@ -271,16 +271,13 @@ Section Exclusive.
       | _, _ => False
     end.
 
-  Global Program Instance ra_eq_equiv : Equivalence ra_res_ex_eq.
-  Next Obligation.
-    intros [t| |]; simpl; now auto.
-  Qed.
-  Next Obligation.
-    intros [t1| |] [t2| |]; simpl; now auto.
-  Qed.
-  Next Obligation.
-    intros [t1| |] [t2| |] [t3| |]; simpl; try now auto.
-    - intros ? ?. etransitivity; eassumption.
+  Global Instance ra_eq_equiv : Equivalence ra_res_ex_eq.
+  Proof.
+    split.
+    - intros [t| |]; simpl; now auto.
+    - intros [t1| |] [t2| |]; simpl; now auto.
+    - intros [t1| |] [t2| |] [t3| |]; simpl; try now auto.
+      + intros ? ?. etransitivity; eassumption.
   Qed.
 
   Global Program Instance ra_type_ex : Setoid ra_res_ex :=
diff --git a/masks.v b/masks.v
index c20ae8ae4..4fc39102f 100644
--- a/masks.v
+++ b/masks.v
@@ -1,4 +1,5 @@
 Require Import Arith Program RelationClasses Morphisms.
+Require Import ModuRes.CSetoid.
 
 Definition mask := nat -> Prop.
 
@@ -28,8 +29,16 @@ Definition mcup (m1 m2 : mask) : mask :=
 Definition mminus (m1 m2 : mask) : mask :=
   fun i => (m1 : mask) i /\ ~ (m2 : mask) i.
 
+Global Instance meq_Equivalence: Equivalence meq.
+Proof.
+  split.
+  - intros m. unfold meq. tauto.
+  - intros m1 m2. unfold meq. now auto.
+  - intros m1 m2 m3. unfold meq. now firstorder.
+Qed.
+Global Instance mask_type : Setoid mask := mkType meq.
+
 Delimit Scope mask_scope with mask.
-Notation "m1 == m2" := (meq m1 m2) (at level 70) : mask_scope.
 Notation "m1 ⊆ m2"  := (mle m1 m2)  (at level 70) : mask_scope.
 Notation "m1 ∩ m2" := (mcap m1 m2) (at level 40) : mask_scope.
 Notation "m1 \  m2"  := (mminus m1 m2) (at level 30) : mask_scope.
-- 
GitLab