fix compatibility with latest Coq master

theories/lifetime/at_borrow.v

@@ -18,7 +18,7 @@ Section atomic_bors.
   Proof. solve_proper. Qed.
   Global Instance at_bor_contractive κ : Contractive (at_bor κ N).
   Proof. solve_contractive. Qed.
-  Global Instance at_bor_proper : Proper ((⊣⊢) ==> (⊣⊢)) (at_bor κ N).
+  Global Instance at_bor_proper κ : Proper ((⊣⊢) ==> (⊣⊢)) (at_bor κ N).
   Proof. solve_proper. Qed.
 
   Lemma at_bor_iff κ P' : ▷ □ (P ↔ P') -∗ &at{κ, N} P -∗ &at{κ, N} P'.
@@ -27,7 +27,7 @@ Section atomic_bors.
     iApply (idx_bor_iff with "HPP' HP").
   Qed.
 
-  Global Instance at_bor_persistent : Persistent (&at{κ, N} P) := _.
+  Global Instance at_bor_persistent κ N P : Persistent (&at{κ, N} P) := _.
 
   Lemma bor_share E κ :
     N ## lftN → &{κ}P ={E}=∗ &at{κ, N}P.

theories/typing/lib/cell.v

@@ -49,10 +49,10 @@ Section cell.
   Lemma cell_proper' E L ty1 ty2 : eqtype E L ty1 ty2 → eqtype E L (cell ty1) (cell ty2).
   Proof. eapply cell_proper. Qed.
 
-  Global Instance cell_copy :
+  Global Instance cell_copy ty :
     Copy ty → Copy (cell ty).
   Proof.
-    intros ty Hcopy. split; first by intros; simpl; unfold ty_own; apply _.
+    intros Hcopy. split; first by intros; simpl; unfold ty_own; apply _.
     iIntros (κ tid E F l q ??) "#LFT #Hshr Htl Htok". iExists 1%Qp. simpl in *.
     (* Size 0 needs a special case as we can't keep the thread-local invariant open. *)
     destruct (ty_size ty) as [|sz] eqn:Hsz; simpl in *.
@@ -73,7 +73,7 @@ Section cell.
     by iMod ("Hclose" with "Hown Htl") as "[$ $]".
   Qed.
 
-  Global Instance cell_send :
+  Global Instance cell_send ty :
     Send ty → Send (cell ty).
   Proof. by unfold cell, Send. Qed.
 End cell.

theories/typing/lib/rc/rc.v

@@ -71,7 +71,7 @@ Section rc.
       | _ => True
       end)%I.
 
-  Global Instance rc_inv_ne ν γ l n :
+  Global Instance rc_inv_ne tid ν γ l n :
     Proper (type_dist2 n ==> dist n) (rc_inv tid ν γ l).
   Proof.
     solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive || f_equiv).
@@ -86,10 +86,10 @@ Section rc.
               (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
               □ (1.[ν] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†ν]))%I.
 
-  Global Instance rc_persist_persistent : Persistent (rc_persist tid ν γ l ty).
+  Global Instance rc_persist_persistent tid ν γ l ty : Persistent (rc_persist tid ν γ l ty).
   Proof. unfold rc_persist, tc_opaque. apply _. Qed.
 
-  Global Instance rc_persist_ne ν γ l n :
+  Global Instance rc_persist_ne tid ν γ l n :
     Proper (type_dist2 n ==> dist n) (rc_persist tid ν γ l).
   Proof.
     solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||

theories/typing/lib/refcell/refcell.v

@@ -204,9 +204,9 @@ Section refcell.
     eqtype E L ty1 ty2 → eqtype E L (refcell ty1) (refcell ty2).
   Proof. eapply refcell_proper. Qed.
 
-  Global Instance refcell_send :
+  Global Instance refcell_send ty :
     Send ty → Send (refcell ty).
-  Proof. move=>????[|[[]|]]//=. Qed.
+  Proof. move=>???[|[[]|]]//=. Qed.
 End refcell.
 
 Hint Resolve refcell_mono' refcell_proper' : lrust_typing.

theories/typing/lib/rwlock/rwlock.v

@@ -192,14 +192,14 @@ Section rwlock.
 
   (* Apparently, we don't need to require ty to be sync,
      contrarily to Rust's implementation. *)
-  Global Instance rwlock_send :
+  Global Instance rwlock_send ty :
     Send ty → Send (rwlock ty).
-  Proof. move=>????[|[[]|]]//=??. iIntros "[$?]". by iApply send_change_tid. Qed.
+  Proof. move=>???[|[[]|]]//=??. iIntros "[$?]". by iApply send_change_tid. Qed.
 
-  Global Instance rwlock_sync :
+  Global Instance rwlock_sync ty :
     Send ty → Sync ty → Sync (rwlock ty).
   Proof.
-    move=>???????/=. do 2 apply bi.exist_mono=>?. apply bi.sep_mono_r.
+    move=>??????/=. do 2 apply bi.exist_mono=>?. apply bi.sep_mono_r.
     iApply at_bor_iff. iIntros "!> !#". iApply bi.equiv_iff.
     apply bi.exist_proper=>?; do 7 f_equiv; first do 7 f_equiv.
     - do 5 f_equiv. apply bi.equiv_spec; split; iApply send_change_tid.

theories/typing/type.v

@@ -274,7 +274,7 @@ Section type_dist2.
       (∀ κ tid l, ty1.(ty_shr) κ tid l ≡{n}≡ ty2.(ty_shr) κ tid l) →
       type_dist2 n ty1 ty2.
 
-  Global Instance type_dist2_equivalence : Equivalence (type_dist2 n).
+  Global Instance type_dist2_equivalence n : Equivalence (type_dist2 n).
   Proof.
     constructor.
     - by constructor.