From bb4b373d3d4e36a3df31f161c348499d01b3ceb1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 17 Mar 2021 12:55:02 +0100
Subject: [PATCH] fix use of auto-generated names

---
 iris_staging/algebra/list.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/iris_staging/algebra/list.v b/iris_staging/algebra/list.v
index a071da6be..b764171fe 100644
--- a/iris_staging/algebra/list.v
+++ b/iris_staging/algebra/list.v
@@ -436,7 +436,8 @@ Section properties.
     (k, ε) ~l~> (k', m) →
     (l ++ k, ε) ~l~> (l ++ k', replicate (length l) ε ++ m).
   Proof.
-    remember (app_l_local_update l k k' ε m) as HH. clear HeqHH. move: HH.
+    remember (app_l_local_update l k k' ε m) as HH eqn:HeqHH.
+    clear HeqHH. move: HH.
     by rewrite take_nil drop_nil ucmra_unit_left_id.
   Qed.
 
@@ -484,7 +485,7 @@ Section properties.
     move: HLen. clear.
     intros HLen. move: n. apply equiv_dist, list_equiv_lookup.
     intros i. rewrite list_lookup_op.
-    remember length as L.
+    remember length as L eqn:HeqL.
     destruct (decide (i < L m''))%nat as [E|E].
     - subst. apply lookup_lt_is_Some in E as [? HEl].
       rewrite HEl.
-- 
GitLab