From 93c004018287f263d9a8364e43a4776f8c531a5d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 7 Dec 2020 11:27:50 +0100
Subject: [PATCH] mono_nat_update: make first argument implicit

---
 iris/algebra/lib/mono_nat.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/algebra/lib/mono_nat.v b/iris/algebra/lib/mono_nat.v
index 7f6332109..4d95547a9 100644
--- a/iris/algebra/lib/mono_nat.v
+++ b/iris/algebra/lib/mono_nat.v
@@ -79,7 +79,7 @@ Section mono_nat.
   Lemma mono_nat_included q n : mono_nat_lb n ≼ mono_nat_auth q n.
   Proof. apply cmra_included_r. Qed.
 
-  Lemma mono_nat_update n n' :
+  Lemma mono_nat_update {n} n' :
     n ≤ n' →
     mono_nat_auth 1 n ~~> mono_nat_auth 1 n'.
   Proof.
-- 
GitLab