ra_res_ex renamed ex.

iris_check.v

@@ -166,7 +166,7 @@ Module StupidLang : CORE_LANG.
 End StupidLang.
 
 Module TrivialRA : RA_T.
-  Definition res := ra_res_ex unit.
+  Definition res := ex unit.
   Instance res_type : Setoid res := _.
   Instance res_op   : RA_op res := _.
   Instance res_unit : RA_unit res := _.

iris_core.v

@@ -5,14 +5,13 @@ Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finma
 Set Bullet Behavior "Strict Subproofs".
 
 (* Because Coq has a restriction of how to apply functors, we have to hack a bit here.
-   PDS: "a bit"?! Hahaha.
    The hack that involves least work, is to duplicate the definition of our final
    resource type, as a module type (which is how we can use it, circumventing the
    Coq restrictions) and as a module (to show the type can be instantiated). *)
 Module Type IRIS_RES (RL : RA_T) (C : CORE_LANG) <: RA_T.
   Instance state_type : Setoid C.state := discreteType.
 
-  Definition res := (ra_res_ex C.state * RL.res)%type.
+  Definition res := (ex C.state * RL.res)%type.
   Instance res_type : Setoid res := _.
   Instance res_op   : RA_op res := _.
   Instance res_unit : RA_unit res := _.

lib/ModuRes/RA.v

@@ -171,14 +171,14 @@ End Order.
 Section Exclusive.
   Context (T: Type) `{eqT : Setoid T}.
 
-  Inductive ra_res_ex: Type :=
-  | ex_own: T -> ra_res_ex
-  | ex_unit: ra_res_ex
-  | ex_bot: ra_res_ex.
+  Inductive ex: Type :=
+  | ex_own: T -> ex
+  | ex_unit: ex
+  | ex_bot: ex.
 
-  Implicit Types (r s : ra_res_ex).
+  Implicit Types (r s : ex).
 
-  Definition ra_res_ex_eq r s: Prop :=
+  Definition ex_eq r s: Prop :=
     match r, s with
       | ex_own t1, ex_own t2 => t1 == t2
       | ex_unit, ex_unit => True
@@ -186,7 +186,7 @@ Section Exclusive.
       | _, _ => False
     end.
 
-  Global Instance ra_eq_equiv : Equivalence ra_res_ex_eq.
+  Global Instance ra_equiv_ex : Equivalence ex_eq.
   Proof.
     split.
     - intros [t| |]; simpl; now auto.
@@ -195,8 +195,8 @@ Section Exclusive.
       + intros ? ?. etransitivity; eassumption.
   Qed.
 
-  Global Program Instance ra_type_ex : Setoid ra_res_ex :=
-    mkType ra_res_ex_eq.
+  Global Program Instance ra_type_ex : Setoid ex :=
+    mkType ex_eq.
 
   Global Instance ra_unit_ex : RA_unit _ := ex_unit.
   Global Instance ra_op_ex : RA_op _ :=
@@ -213,7 +213,7 @@ Section Exclusive.
                | _      => True
              end.
 
-  Global Instance ra_ex : RA ra_res_ex.
+  Global Instance ra_ex : RA ex.
   Proof.
     split.
     - intros [t1| |] [t2| |] Heqt [t'1| |] [t'2| |] Heqt'; simpl; now auto.