Fix build error in new Coq version

theories/typing/product.v

@@ -202,15 +202,15 @@ Section product.
     iIntros (κ tid1 tid2 ps l) "/=[#Hshr1 #Hshr2]". iSplit; by iApply @sync_change_tid.
   Qed.
 
-  Global Instance product2_drop `{!Drop ty1} `{!Drop ty2} : Drop (product2 ty1 ty2) :=
+  Global Program Instance product2_drop `{!Drop ty1} `{!Drop ty2} : Drop (product2 ty1 ty2) :=
   {| drop_in_place :=
         funrec: <> ["p"] :=
           letcall: "_" := (drop_in_place ty1) ["p"]%E in
           letcall: "_" := (drop_in_place ty2) ["p" +ₗ #(ty_size ty1)]%E in
           return: [ #☠ ];
   |}.
-  Proof.
-    iIntros (???? [?<-]) "#LFT #HE Htl [Hop1 Hop2] Hk /=".
+  Next Obligation.
+    iIntros (???????? [?<-]) "#LFT #HE Htl [Hop1 Hop2] Hk /=".
     do 2 wp_rec. iApply (drop_spec with "LFT HE Htl Hop1").
     iIntros "Htl Hp↦". do 2 wp_rec. wp_op.
     iApply (drop_spec with "LFT HE Htl Hop2").