diff --git a/coq-reloc.opam b/coq-reloc.opam
index 32782902f5de246e935f0e65fe6d72e6dbf079bf..8145453b19f97fe2f7c7956d7c82e066de8fe05e 100644
--- a/coq-reloc.opam
+++ b/coq-reloc.opam
@@ -6,7 +6,7 @@ bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/dfrumin/reloc.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2022-05-13.0.a1971471") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2022-05-13.5.de41b20f") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index e4944d5ca758f785d5a18f6ad9103414556d97f4..09c1d8fe058a19585f5e9bf253c7ecce4f43eb3f 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -138,7 +138,7 @@ Section rules.
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
     iDestruct "Hinv" as (ρ) "Hinv".
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
-    destruct (exist_fresh (dom (D:=gset _) (heap σ))) as [l Hl%not_elem_of_dom].
+    destruct (exist_fresh (dom (heap σ))) as [l Hl%not_elem_of_dom].
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
diff --git a/theories/typing/types.v b/theories/typing/types.v
index 5b8d9f099b742cff41b4a825b60b3acdc7b3a0b2..3813d83e54a1704dba28acdff9df2b634df367fe 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -313,7 +313,7 @@ Proof.
         revert typed_is_closed_set. by rewrite dom_insert_L.
       * specialize (typed_is_closed_set _ e Ï„2 H).
         revert typed_is_closed_set.
-        rewrite (dom_insert_L (D:=stringset) (<[x:=τ1]> Γ) f (τ1→τ2)%ty).
+        rewrite (dom_insert_L (<[x:=τ1]> Γ) f (τ1→τ2)%ty).
         by rewrite dom_insert_L.
     + specialize (typed_is_closed_set (⤉Γ) e τ H).
       revert typed_is_closed_set. by rewrite dom_fmap_L.
@@ -324,7 +324,7 @@ Proof.
       ++ specialize (typed_is_closed_set _ _ _ H0).
          revert typed_is_closed_set. by rewrite dom_fmap_L.
       ++ specialize (typed_is_closed_set _ _ _ H0).
-         revert typed_is_closed_set. rewrite (dom_insert_L (D:=stringset) (⤉Γ) x).
+         revert typed_is_closed_set. rewrite (dom_insert_L (⤉Γ) x).
          by rewrite dom_fmap_L.
   - induction 1; simplify_eq/=; try done.
     + by split_and?.
@@ -335,11 +335,11 @@ Proof.
         revert typed_is_closed_set. by rewrite dom_insert_L dom_empty_L.
       * specialize (typed_is_closed_set _ _ _ H).
         revert typed_is_closed_set.
-        rewrite (dom_insert_L (D:=stringset) _ f (τ1→τ2)%ty).
+        rewrite (dom_insert_L _ f (τ1→τ2)%ty).
         by rewrite dom_empty_L.
       * specialize (typed_is_closed_set _ _ _ H).
         revert typed_is_closed_set.
-        rewrite (dom_insert_L (D:=stringset) (<[x:=τ1]> ∅) f (τ1→τ2)%ty).
+        rewrite (dom_insert_L (<[x:=τ1]> ∅) f (τ1→τ2)%ty).
         by rewrite dom_insert_L dom_empty_L.
     + specialize (typed_is_closed_set _ _ _ H).
       revert typed_is_closed_set. by rewrite dom_empty_L.