From a529364ee192891878260f3f8f8f7bdccd4554ce Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 7 Jun 2021 11:19:11 +0200
Subject: [PATCH] =?UTF-8?q?Global=20Lemma=20=E2=86=92=20Lemma?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 iris_staging/algebra/max_prefix_list.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris_staging/algebra/max_prefix_list.v b/iris_staging/algebra/max_prefix_list.v
index ec1b0c2af..30f35f7c2 100644
--- a/iris_staging/algebra/max_prefix_list.v
+++ b/iris_staging/algebra/max_prefix_list.v
@@ -39,12 +39,12 @@ Section max_prefix_list.
 
   Global Instance mono_list_lb_core_id (m : max_prefix_list A) : CoreId m := _.
 
-  Global Lemma to_max_prefix_list_valid l : ✓ to_max_prefix_list l.
+  Lemma to_max_prefix_list_valid l : ✓ to_max_prefix_list l.
   Proof.
     intros i. rewrite /to_max_prefix_list lookup_fmap.
     by destruct (map_seq 0 l !! i).
   Qed.
-  Global Lemma to_max_prefix_list_validN n l : ✓{n} to_max_prefix_list l.
+  Lemma to_max_prefix_list_validN n l : ✓{n} to_max_prefix_list l.
   Proof. apply cmra_valid_validN, to_max_prefix_list_valid. Qed.
 
   Local Lemma to_max_prefix_list_app l1 l2 :
-- 
GitLab