Skip to content
Snippets Groups Projects
Commit 287cfd91 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Avoid slow `try done`.

parent 26d4f967
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/program_logic/total_adequacy.v
+ 1
− 1
View file @ 287cfd91
...@@ -51,7 +51,7 @@ Proof. ...@@ -51,7 +51,7 @@ Proof.
iIntros (t1 t1' Ht) "Ht1". iRevert (t1' Ht); iRevert (t1) "Ht1". iIntros (t1 t1' Ht) "Ht1". iRevert (t1' Ht); iRevert (t1) "Ht1".
iApply twptp_ind; iIntros "!>" (t1) "IH"; iIntros (t1' Ht). iApply twptp_ind; iIntros "!>" (t1) "IH"; iIntros (t1' Ht).
rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 κ κs σ2 n Hstep) "Hσ". 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 & _)". iMod ("IH" $! t2' with "[% //] Hσ") as (n2) "($ & Hσ & IH & _)".
iModIntro. iExists n2. iFrame "Hσ". by iApply "IH". iModIntro. iExists n2. iFrame "Hσ". by iApply "IH".
Qed. Qed.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment