From 0d9d1b8384b55ace48da91a2cfb96e559bcba1dc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 23 Jul 2021 18:30:47 +0200
Subject: [PATCH] compatibility with Coq master (Coq PR 14606)

---
 theories/typing/fixpoint.v                    |  4 ++--
 theories/typing/function.v                    |  2 +-
 theories/typing/lib/arc.v                     |  6 +++---
 theories/typing/lib/cell.v                    |  2 +-
 theories/typing/lib/mutex/mutex.v             |  2 +-
 theories/typing/lib/mutex/mutexguard.v        |  2 +-
 theories/typing/lib/rc/rc.v                   |  4 ++--
 theories/typing/lib/rc/weak.v                 |  2 +-
 theories/typing/lib/refcell/ref.v             |  2 +-
 theories/typing/lib/refcell/refcell.v         |  2 +-
 theories/typing/lib/refcell/refmut.v          |  2 +-
 theories/typing/lib/rwlock/rwlock.v           |  2 +-
 theories/typing/lib/rwlock/rwlockreadguard.v  |  2 +-
 theories/typing/lib/rwlock/rwlockwriteguard.v |  2 +-
 theories/typing/lib/spawn.v                   |  2 +-
 theories/typing/own.v                         |  2 +-
 theories/typing/shr_bor.v                     |  2 +-
 theories/typing/type.v                        | 12 ++++++------
 theories/typing/uniq_bor.v                    |  2 +-
 19 files changed, 28 insertions(+), 28 deletions(-)

diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index dc64f4ae..fa8f989e 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -28,11 +28,11 @@ Section fixpoint_def.
   Global Instance type_fixpoint_wf `{!∀ `{!TyWf ty}, TyWf (T ty)} : TyWf type_fixpoint :=
     let lfts :=
       let _ : TyWf type_fixpoint := {| ty_lfts := []; ty_wf_E := [] |} in
-      (T type_fixpoint).(ty_lfts)
+      ty_lfts (T type_fixpoint)
     in
     let wf_E :=
       let _ : TyWf type_fixpoint := {| ty_lfts := lfts; ty_wf_E := [] |} in
-      (T type_fixpoint).(ty_wf_E)
+      ty_wf_E (T type_fixpoint)
     in
     {| ty_lfts := lfts; ty_wf_E := wf_E |}.
 End fixpoint_def.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 3faa1a71..246d4334 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -12,7 +12,7 @@ Section fn.
 
   Definition FP_wf E (tys : vec type n) `{!ListTyWf tys} ty `{!TyWf ty} :=
     FP (λ ϝ, E ϝ ++ tyl_wf_E tys ++ tyl_outlives_E tys ϝ ++
-                    ty.(ty_wf_E) ++ ty_outlives_E ty ϝ)
+                    ty_wf_E ty ++ ty_outlives_E ty ϝ)
        tys ty.
 
   (* The other alternative for defining the fn type would be to state
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index f584e7c5..e976a095 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -221,7 +221,7 @@ Section arc.
   Qed.
 
   Global Instance arc_wf ty `{!TyWf ty} : TyWf (arc ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Global Instance arc_type_contractive : TypeContractive arc.
   Proof.
@@ -346,7 +346,7 @@ Section arc.
   Qed.
 
   Global Instance weak_wf ty `{!TyWf ty} : TyWf (weak ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Global Instance weak_type_contractive : TypeContractive weak.
   Proof.
@@ -941,7 +941,7 @@ Section arc.
   (* Code : other primitives *)
   Definition arc_try_unwrap ty : val :=
     fn: ["arc"] :=
-      let: "r" := new [ #(Σ[ ty; arc ty ]).(ty_size) ] in
+      let: "r" := new [ #(ty_size Σ[ ty; arc ty ]) ] in
       let: "arc'" := !"arc" in
       if: try_unwrap ["arc'"] then
         (* Return content *)
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 9754ad21..514fbd75 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -21,7 +21,7 @@ Section cell.
   Qed.
 
   Global Instance cell_wf ty `{!TyWf ty} : TyWf (cell ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Global Instance cell_type_ne : TypeNonExpansive cell.
   Proof. solve_type_proper. Qed.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 6452d0de..6d4f1997 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -67,7 +67,7 @@ Section mutex.
   Qed.
 
   Global Instance mutex_wf ty `{!TyWf ty} : TyWf (mutex ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Global Instance mutex_type_ne : TypeNonExpansive mutex.
   Proof.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 471c21e6..6cb50d72 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -72,7 +72,7 @@ Section mguard.
   Qed.
 
   Global Instance mutexguard_wf α ty `{!TyWf ty} : TyWf (mutexguard α ty) :=
-    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty α }.
+    { ty_lfts := [α]; ty_wf_E := ty_wf_E ty ++ ty_outlives_E ty α }.
 
   Global Instance mutexguard_type_contractive α : TypeContractive (mutexguard α).
   Proof.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index d3c5b194..193629bb 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -201,7 +201,7 @@ Section rc.
   Qed.
 
   Global Instance rc_wf ty `{!TyWf ty} : TyWf (rc ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Global Instance rc_type_contractive : TypeContractive rc.
   Proof.
@@ -659,7 +659,7 @@ Section code.
 
   Definition rc_try_unwrap ty : val :=
     fn: ["rc"] :=
-      let: "r" := new [ #(Σ[ ty; rc ty ]).(ty_size) ] in
+      let: "r" := new [ #(ty_size Σ[ ty; rc ty ]) ] in
     withcont: "k":
       let: "rc'" := !"rc" in
       let: "strong" := !("rc'" +â‚— #0) in
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 6df9fa67..b6c6befb 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -71,7 +71,7 @@ Section weak.
   Qed.
 
   Global Instance weak_wf ty `{!TyWf ty} : TyWf (weak ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Global Instance weak_type_contractive : TypeContractive weak.
   Proof.
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index 8c3e2f0c..7de2d426 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -69,7 +69,7 @@ Section ref.
   Qed.
 
   Global Instance ref_wf α ty `{!TyWf ty} : TyWf (ref α ty) :=
-    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty α }.
+    { ty_lfts := [α]; ty_wf_E := ty_wf_E ty ++ ty_outlives_E ty α }.
 
   Global Instance ref_type_contractive α : TypeContractive (ref α).
   Proof. solve_type_proper. Qed.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 6d60ef56..413bb764 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -164,7 +164,7 @@ Section refcell.
   Qed.
 
   Global Instance refcell_wf ty `{!TyWf ty} : TyWf (refcell ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Global Instance refcell_type_ne : TypeNonExpansive refcell.
   Proof.
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 65cd958d..57402d42 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -74,7 +74,7 @@ Section refmut.
   Qed.
 
   Global Instance refmut_wf α ty `{!TyWf ty} : TyWf (refmut α ty) :=
-    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty α }.
+    { ty_lfts := [α]; ty_wf_E := ty_wf_E ty ++ ty_outlives_E ty α }.
 
   Global Instance refmut_type_contractive α : TypeContractive (refmut α).
   Proof. solve_type_proper. Qed.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 5c4f50cd..f1e71df7 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -415,7 +415,7 @@ Section rwlock.
   Qed.
 
   Global Instance rwlock_wf ty `{!TyWf ty} : TyWf (rwlock ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Global Instance rwlock_type_ne : TypeNonExpansive rwlock.
   Proof.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 8e291043..af08b2af 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -63,7 +63,7 @@ Section rwlockreadguard.
   Qed.
 
   Global Instance rwlockreadguard_wf α ty `{!TyWf ty} : TyWf (rwlockreadguard α ty) :=
-    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty α }.
+    { ty_lfts := [α]; ty_wf_E := ty_wf_E ty ++ ty_outlives_E ty α }.
 
   Global Instance rwlockreadguard_type_contractive α : TypeContractive (rwlockreadguard α).
   Proof.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 77b1f438..368a7b60 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -65,7 +65,7 @@ Section rwlockwriteguard.
   Qed.
 
   Global Instance rwlockwriteguard_wf α ty `{!TyWf ty} : TyWf (rwlockwriteguard α ty) :=
-    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty α }.
+    { ty_lfts := [α]; ty_wf_E := ty_wf_E ty ++ ty_outlives_E ty α }.
 
   Global Instance rwlockwriteguard_type_contractive α : TypeContractive (rwlockwriteguard α).
   Proof.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index eb57e95f..c88073a9 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -25,7 +25,7 @@ Section join_handle.
   Next Obligation. iIntros (?) "**"; auto. Qed.
 
   Global Instance join_handle_wf ty `{!TyWf ty} : TyWf (join_handle ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Lemma join_handle_subtype ty1 ty2 :
     ▷ type_incl ty1 ty2 -∗ type_incl (join_handle ty1) (join_handle ty2).
diff --git a/theories/typing/own.v b/theories/typing/own.v
index f14a983c..27dbbb06 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -88,7 +88,7 @@ Section own.
   Qed.
 
   Global Instance own_ptr_wf n ty `{!TyWf ty} : TyWf (own_ptr n ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Lemma own_type_incl n m ty1 ty2 :
     ▷ ⌜n = m⌝ -∗ ▷ type_incl ty1 ty2 -∗ type_incl (own_ptr n ty1) (own_ptr m ty2).
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index e6042d95..1b723d93 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -16,7 +16,7 @@ Section shr_bor.
   Next Obligation. intros κ ty tid [|[[]|][]]; apply _. Qed.
 
   Global Instance shr_bor_wf κ ty `{!TyWf ty} : TyWf (shr_bor κ ty) :=
-    { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty κ }.
+    { ty_lfts := [κ]; ty_wf_E := ty_wf_E ty ++ ty_outlives_E ty κ }.
 
   Lemma shr_type_incl κ1 κ2 ty1 ty2 :
     κ2 ⊑ κ1 -∗ type_incl ty1 ty2 -∗ type_incl (shr_bor κ1 ty1) (shr_bor κ2 ty2).
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 183eb2d2..f1d22fad 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -62,14 +62,14 @@ Arguments ty_lfts {_ _} _ {_}.
 Arguments ty_wf_E {_ _} _ {_}.
 
 Definition ty_outlives_E `{!typeG Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
-  (λ α, κ ⊑ₑ α) <$> ty.(ty_lfts).
+  (λ α, κ ⊑ₑ α) <$> (ty_lfts ty).
 
 Lemma ty_outlives_E_elctx_sat `{!typeG Σ} E L ty `{!TyWf ty} α β :
   ty_outlives_E ty β ⊆+ E →
   lctx_lft_incl E L α β →
   elctx_sat E L (ty_outlives_E ty α).
 Proof.
-  unfold ty_outlives_E. induction ty.(ty_lfts) as [|κ l IH]=>/= Hsub Hαβ.
+  unfold ty_outlives_E. induction (ty_lfts ty) as [|κ l IH]=>/= Hsub Hαβ.
   - solve_typing.
   - apply elctx_sat_lft_incl.
     + etrans; first done. eapply lctx_lft_incl_external, elem_of_submseteq, Hsub.
@@ -87,15 +87,15 @@ Existing Instances list_ty_wf_nil list_ty_wf_cons.
 Fixpoint tyl_lfts `{!typeG Σ} tyl {WF : ListTyWf tyl} : list lft :=
   match WF with
   | list_ty_wf_nil => []
-  | list_ty_wf_cons ty [] => ty.(ty_lfts)
-  | list_ty_wf_cons ty tyl => ty.(ty_lfts) ++ tyl.(tyl_lfts)
+  | list_ty_wf_cons ty [] => ty_lfts ty
+  | list_ty_wf_cons ty tyl => ty_lfts ty ++ tyl_lfts tyl
   end.
 
 Fixpoint tyl_wf_E `{!typeG Σ} tyl {WF : ListTyWf tyl} : elctx :=
   match WF with
   | list_ty_wf_nil => []
-  | list_ty_wf_cons ty [] => ty.(ty_wf_E)
-  | list_ty_wf_cons ty tyl => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
+  | list_ty_wf_cons ty [] => ty_wf_E ty
+  | list_ty_wf_cons ty tyl => ty_wf_E ty ++ tyl_wf_E tyl
   end.
 
 Fixpoint tyl_outlives_E `{!typeG Σ} tyl {WF : ListTyWf tyl} (κ : lft) : elctx :=
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 4747f0f7..40f68513 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -41,7 +41,7 @@ Section uniq_bor.
   Qed.
 
   Global Instance uniq_bor_wf κ ty `{!TyWf ty} : TyWf (uniq_bor κ ty) :=
-    { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty κ }.
+    { ty_lfts := [κ]; ty_wf_E := ty_wf_E ty ++ ty_outlives_E ty κ }.
 
   Lemma uniq_type_incl κ1 κ2 ty1 ty2 :
     κ2 ⊑ κ1 -∗
-- 
GitLab