From 03a7eae7923deac0a824eb524ce7692f20f1833b Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Tue, 22 Mar 2022 11:30:32 +0100
Subject: [PATCH] Avoided use of [apply:] as Coq it caused 8.15.0 looping
behaviour
---
theories/channel/proto.v | 6 ++++--
theories/channel/proto_model.v | 3 ++-
2 files changed, 6 insertions(+), 3 deletions(-)
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index f0319c0..63eeb95 100644
--- a/theories/channel/proto.v
+++ b/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).
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index 2d5ddb4..0a9bf8d 100644
--- a/theories/channel/proto_model.v
+++ b/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}
--
GitLab