From 778f323153c253ac767ef8dae649d589c18e4593 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Mon, 25 Apr 2022 19:33:17 +0200
Subject: [PATCH] Added priotity to swap rule of proofmode to avoid looping TC
 search

---
 theories/channel/proofmode.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 2005837..dfda68a 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -135,7 +135,7 @@ Section classes.
     (∀.. x1, MsgTele (tele_app tm1 x1) tv2 tP2 (tele_app tp x1)) →
     ProtoNormalize d (<a> m) pas (<!.. x2> MSG tele_app tv2 x2 {{ tele_app tP2 x2 }};
                                   <?.. x1> MSG tele_app tv1 x1 {{ tele_app tP1 x1 }};
-                                  tele_app (tele_app tp x1) x2).
+                                  tele_app (tele_app tp x1) x2) | 1.
   Proof.
     rewrite /ActionDualIf /MsgNormalize /ProtoNormalize /MsgTele.
     rewrite tforall_forall=> Ha Hm Hm' Hm''.
-- 
GitLab