bump Iris

semantics.opam

@@ -10,7 +10,7 @@ version: "dev"
 
 depends: [
   "coq" { (>= "8.13" & < "8.17~") | (= "dev") }
-  "coq-iris-heap-lang" { (= "dev.2023-03-07.1.7e127436") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-03-18.3.1b3e86bb") | (= "dev") }
   "coq-equations" { (= "1.2.4+8.13") | (= "1.3+8.14") | (= "1.3+8.15")  | (= "1.3+8.16") }
   "coq-autosubst" { (= "1.7") | (= "dev")  }
 ]

theories/program_logics/heap_lang/derived_laws.v

@@ -53,20 +53,20 @@ Lemma array_nil l dq : l ↦∗{dq} [] ⊣⊢ emp.
 Proof. by rewrite /array. Qed.
 
 Lemma array_singleton l dq v : l ↦∗{dq} [v] ⊣⊢ l ↦{dq} v.
-Proof. by rewrite /array /= right_id loc_add_0. Qed.
+Proof. by rewrite /array /= right_id Loc.add_0. Qed.
 
 Lemma array_app l dq vs ws :
   l ↦∗{dq} (vs ++ ws) ⊣⊢ l ↦∗{dq} vs ∗ (l +ₗ length vs) ↦∗{dq} ws.
 Proof.
   rewrite /array big_sepL_app.
   setoid_rewrite Nat2Z.inj_add.
-  by setoid_rewrite loc_add_assoc.
+  by setoid_rewrite Loc.add_assoc.
 Qed.
 
 Lemma array_cons l dq v vs : l ↦∗{dq} (v :: vs) ⊣⊢ l ↦{dq} v ∗ (l +ₗ 1) ↦∗{dq} vs.
 Proof.
-  rewrite /array big_sepL_cons loc_add_0.
-  setoid_rewrite loc_add_assoc.
+  rewrite /array big_sepL_cons Loc.add_0.
+  setoid_rewrite Loc.add_assoc.
   setoid_rewrite Nat2Z.inj_succ.
   by setoid_rewrite Z.add_1_l.
 Qed.
@@ -104,7 +104,7 @@ Proof.
   { done. }
   iIntros "[$ Hl]". rewrite -fmap_S_seq big_sepL_fmap.
   setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
-  setoid_rewrite <-loc_add_assoc. iApply "IH". done.
+  setoid_rewrite <-Loc.add_assoc. iApply "IH". done.
 Qed.
 
 Lemma wp_allocN s E v n Φ :

theories/program_logics/heap_lang/primitive_laws.v

@@ -97,10 +97,10 @@ Proof.
   rewrite big_opM_union; last first.
   { apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
     intros (j&w&?&Hjl&_)%heap_array_lookup.
-    rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
-  rewrite loc_add_0 -fmap_S_seq big_sepL_fmap.
+    rewrite Loc.add_assoc -{1}[l']Loc.add_0 in Hjl. simplify_eq; lia. }
+  rewrite Loc.add_0 -fmap_S_seq big_sepL_fmap.
   setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
-  setoid_rewrite <-loc_add_assoc.
+  setoid_rewrite <-Loc.add_assoc.
   rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]". by iApply "IH".
 Qed.
 
@@ -128,7 +128,7 @@ Lemma wp_alloc s E v Φ :
   WP Alloc (Val v) @ s; E; E {{ Φ }}.
 Proof.
   iIntros "HΦ". iApply wp_allocN_seq; [auto with lia..|].
-  iIntros "!>" (l) "/= (? & _)". rewrite loc_add_0. iApply "HΦ"; iFrame.
+  iIntros "!>" (l) "/= (? & _)". rewrite Loc.add_0. iApply "HΦ"; iFrame.
 Qed.
 
 Lemma wp_free s E l v Φ :

theories/program_logics/reloc/src_rules.v

@@ -224,7 +224,7 @@ Section rules.
     You will find the following lemmas relating to memory allocation helpful:
     - alloc_fresh
     - state_init_heap_singleton
-    - fresh_locs_fresh
+    - Loc.fresh_fresh
     - not_elem_of_dom
     - loc_add_0_l
      *)