From 890a7ae5dde9a279d5ec65430680377a8100584d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 13 May 2022 17:43:07 +0200
Subject: [PATCH] update dependencies

some type annotations are no longer needed
---
 coq-reloc.opam              | 2 +-
 theories/logic/spec_rules.v | 2 +-
 theories/typing/types.v     | 8 ++++----
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/coq-reloc.opam b/coq-reloc.opam
index 3278290..8145453 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 e4944d5..09c1d8f 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 5b8d9f0..3813d83 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.
-- 
GitLab