From 287cfd910a9d04eec4fcdce5a3b4afa9c2e0723b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 18 Mar 2020 20:36:44 +0100
Subject: [PATCH] Avoid slow `try done`.

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

diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index c3d0235b9..774dbf1d7 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -51,7 +51,7 @@ Proof.
   iIntros (t1 t1' Ht) "Ht1". iRevert (t1' Ht); iRevert (t1) "Ht1".
   iApply twptp_ind; iIntros "!>" (t1) "IH"; iIntros (t1' Ht).
   rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 κ κs σ2 n Hstep) "Hσ".
-  destruct (step_Permutation t1' t1 t2 κ σ1 σ2) as (t2'&?&?); try done.
+  destruct (step_Permutation t1' t1 t2 κ σ1 σ2) as (t2'&?&?); [done..|].
   iMod ("IH" $! t2' with "[% //] Hσ") as (n2) "($ & Hσ & IH & _)".
   iModIntro. iExists n2. iFrame "Hσ". by iApply "IH".
 Qed.
-- 
GitLab