From d20b33242f07d817c8a2765aab44df812ab7d660 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 1 May 2020 11:30:27 +0200
Subject: [PATCH] Nit
---
theories/logrel/subtyping_rules.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 6c6a27b..31beeb3 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -298,7 +298,7 @@ Section subtyping_rules.
iApply iProto_le_trans;
[iApply iProto_le_base; iApply (iProto_le_exist_intro_l _ x2)|]; simpl.
iApply iProto_le_payload_elim_r.
- iMod 1 as "%". revert H1.
+ iMod 1 as %HSs. revert HSs.
rewrite !lookup_total_alt !lookup_fmap fmap_is_Some; iIntros ([S ->]) "/=".
iApply iProto_le_trans; [iApply iProto_le_base_swap|]. iSplitL; [by eauto|].
iModIntro. by iExists v1.
--
GitLab