From 20ce8454a8e6169481cbb32e0d54f5ea6777ba40 Mon Sep 17 00:00:00 2001 From: jihgfee <jihgfee@gmail.com> Date: Tue, 14 Apr 2020 14:59:20 +0200 Subject: [PATCH] Nits --- theories/logrel/subtyping.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v index 9fe1c1c..6b6df0d 100644 --- a/theories/logrel/subtyping.v +++ b/theories/logrel/subtyping.v @@ -242,7 +242,7 @@ Section subtype. Ps2 ⊆ Ps1 → ⊢ lsty_select Ps1 <p: lsty_select Ps2. Proof. - iIntros (Hnone) "!>". + iIntros (Hsub) "!>". iApply iProto_le_send. iIntros (x) ">% !>"=> /=. iExists _. iSplit=> //. @@ -279,7 +279,7 @@ Section subtype. Ps1 ⊆ Ps2 → ⊢ lsty_branch Ps1 <p: lsty_branch Ps2. Proof. - iIntros (Hnone) "!>". + iIntros (Hsub) "!>". iApply iProto_le_recv. iIntros (x) ">% !>"=> /=. iExists _. iSplit=> //. -- GitLab