From 9eae1e7121fe88ac86bb80ce6aaebf693dbc5852 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 4 Dec 2020 21:01:07 +0100
Subject: [PATCH] Improve implicit arguments.

---
 iris/base_logic/lib/mono_nat.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index edb87d413..620da1cc5 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -89,7 +89,7 @@ Section mono_nat.
     mono_nat_auth_own γ q n -∗ mono_nat_lb_own γ n.
   Proof. unseal. apply own_mono, mono_nat_included. Qed.
 
-  Lemma mono_nat_lb_own_le γ n n' :
+  Lemma mono_nat_lb_own_le {γ n} n' :
     n' ≤ n →
     mono_nat_lb_own γ n -∗ mono_nat_lb_own γ n'.
   Proof. unseal. intros. by apply own_mono, mono_nat_lb_mono. Qed.
@@ -102,7 +102,7 @@ Section mono_nat.
     auto with iFrame.
   Qed.
 
-  Lemma mono_nat_own_update γ n n' :
+  Lemma mono_nat_own_update {γ n} n' :
     n ≤ n' →
     mono_nat_auth_own γ 1 n ==∗ mono_nat_auth_own γ 1 n' ∗ mono_nat_lb_own γ n'.
   Proof.
-- 
GitLab