From 75f6aaaeb4203e01ebe01b2e32add098bc07d8d7 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sat, 1 May 2021 22:25:31 +0200
Subject: [PATCH] Nit.
---
theories/typing/sum.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index ebf0d432..82f1a461 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -1,6 +1,7 @@
From iris.proofmode Require Import tactics.
From iris.algebra Require Import list.
From iris.bi Require Import fractional.
+From lrust.typing Require Import lft_contexts.
From lrust.typing Require Export type.
Set Default Proof Using "Type".
@@ -126,7 +127,7 @@ Section sum.
Proper (Forall2 (subtype E L) ==> subtype E L) sum.
Proof.
iIntros (tyl1 tyl2 Htyl qmax qL) "HL".
- iAssert (□ (lft_contexts.elctx_interp E -∗ ⌜max_list_with ty_size tyl1 = max_list_with ty_size tyl2⌝))%I with "[#]" as "#Hleq".
+ iAssert (□ (elctx_interp E -∗ ⌜max_list_with ty_size tyl1 = max_list_with ty_size tyl2⌝))%I with "[#]" as "#Hleq".
{ iInduction Htyl as [|???? Hsub] "IH".
{ iClear "∗". iIntros "!# _". done. }
iDestruct (Hsub with "HL") as "#Hsub". iDestruct ("IH" with "HL") as "{IH} #IH".
--
GitLab