Avoided use of [apply:] as Coq it caused 8.15.0 looping behaviour

theories/channel/proto.v

@@ -493,7 +493,8 @@ Section proto.
   Proof.
     rewrite iProto_message_eq iProto_dual_eq /iProto_dual_def /iProto_map_app.
     etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
-    apply: proto_elim_message=> a' m1 m2 Hm; f_equiv; solve_proper.
+    rewrite /iProto_message_def. rewrite ->proto_elim_message; [done|].
+    intros a' m1 m2 Hm; f_equiv; solve_proper.
   Qed.
   Lemma iMsg_dual_base v P p :
     iMsg_dual (MSG v {{ P }}; p) ≡ (MSG v {{ P }}; iProto_dual p)%msg.
@@ -529,7 +530,8 @@ Section proto.
   Proof.
     rewrite iProto_message_eq iProto_app_eq /iProto_app_def /iProto_map_app.
     etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
-    apply: proto_elim_message=> a' m1 m2 Hm. f_equiv; solve_proper.
+    rewrite /iProto_message_def. rewrite ->proto_elim_message; [done|].
+    intros a' m1 m2 Hm. f_equiv; solve_proper.
   Qed.
 
   Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ V).

theories/channel/proto_model.v

@@ -224,7 +224,8 @@ Lemma proto_map_message {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'
   ≡ proto_message a (λ v, g ◎ m v ◎ laterO_map (proto_map g gn)).
 Proof.
   rewrite proto_map_unfold /proto_map_aux /=.
-  apply: proto_elim_message=> a' m1 m2 Hm; f_equiv; solve_proper.
+  rewrite ->proto_elim_message; [done|].
+  intros a' m1 m2 Hm. f_equiv; solve_proper.
 Qed.
 
 Lemma proto_map_ne {V}