From 2324573916f03191a9431dbad1a56e07c4b795dd Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 21 Mar 2021 14:10:13 +0100
Subject: [PATCH] avoid relying on failing destruct of existential

---
 theories/typing/interp.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 403a9ed..d69bf6f 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -51,9 +51,9 @@ Section semtypes.
     interp τ Δ v v' -∗ ⌜val_is_unboxed v ∧ val_is_unboxed v'⌝.
   Proof.
     induction 1; simpl;
-    first [iIntros "[% %]"
+    first [iDestruct 1 as (? ?) "[% [% ?]]"
           |iDestruct 1 as (?) "[% %]"
-          |iDestruct 1 as (? ?) "[% [% ?]]"];
+          |iIntros "[% %]"];
     simplify_eq/=; eauto with iFrame.
   Qed.
 
-- 
GitLab