From 6946d01b181c7bebf3fac50f9e55c4a9fa67e9dc 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/ghostcell.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 +-
 20 files changed, 29 insertions(+), 29 deletions(-)

diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index b35258a6..01ffd0e5 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 9eed7c5e..cba36f42 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -11,7 +11,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 0cf17a54..b1dcc976 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -161,7 +161,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.
@@ -274,7 +274,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.
@@ -837,7 +837,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 9645ecbd..104a1a2c 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/ghostcell.v b/theories/typing/lib/ghostcell.v
index 7085874b..b66130a0 100644
--- a/theories/typing/lib/ghostcell.v
+++ b/theories/typing/lib/ghostcell.v
@@ -321,7 +321,7 @@ Section ghostcell.
   Qed.
 
   Global Instance ghostcell_wf α `{!TyWf ty} : TyWf (ghostcell α 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 ghostcell_type_ne α : TypeNonExpansive (ghostcell α).
   Proof.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index ca3cd06d..65bbe7f9 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -73,7 +73,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 960c7464..6ee38f83 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -73,7 +73,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 2f725829..10c15e91 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -194,7 +194,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.
@@ -652,7 +652,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 a218e1de..b9ad6cd0 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -65,7 +65,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 7ee34cc9..cd37e6b8 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -70,7 +70,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 15ffbb55..7ccd3888 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -165,7 +165,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 b405995b..2549cc0d 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -75,7 +75,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 ad9ef92c..77130248 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -172,7 +172,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 51df1e84..d4741c21 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 702201bc..620afee4 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -63,7 +63,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 421bb191..6fc0af6b 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 757e883c..c0db77cf 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -87,7 +87,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 0fb7bf7f..360c9672 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 ea9fa413..33339544 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -57,14 +57,14 @@ Arguments ty_lfts {_ _} _ {_}.
 Arguments ty_wf_E {_ _} _ {_}.
 
 Definition ty_outlives_E `{!typeGS Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
-  (λ α, κ ⊑ₑ α) <$> ty.(ty_lfts).
+  (λ α, κ ⊑ₑ α) <$> (ty_lfts ty).
 
 Lemma ty_outlives_E_elctx_sat `{!typeGS Σ} 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.
@@ -82,15 +82,15 @@ Existing Instances list_ty_wf_nil list_ty_wf_cons.
 Fixpoint tyl_lfts `{!typeGS Σ} 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 `{!typeGS Σ} 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 `{!typeGS Σ} tyl {WF : ListTyWf tyl} (κ : lft) : elctx :=
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 3813dd68..742c8c95 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -42,7 +42,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