From f1cefaacce27a67cd76d3cbf7f320431d2306f9b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Mon, 8 Aug 2022 14:28:48 +0000
Subject: [PATCH] more space

---
 iris/algebra/lib/mono_list.v | 2 +-
 iris/algebra/lib/mono_nat.v  | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/iris/algebra/lib/mono_list.v b/iris/algebra/lib/mono_list.v
index 68177aa69..5c9b0c039 100644
--- a/iris/algebra/lib/mono_list.v
+++ b/iris/algebra/lib/mono_list.v
@@ -70,7 +70,7 @@ Section mono_list_props.
 
   Global Instance mono_list_auth_dfrac_is_op dq dq1 dq2 l :
     IsOp dq dq1 dq2 → IsOp' (●ML{dq} l) (●ML{dq1} l) (●ML{dq2} l).
-  Proof. rewrite /IsOp' /IsOp=>->. rewrite mono_list_auth_dfrac_op //. Qed.
+  Proof. rewrite /IsOp' /IsOp=> ->. rewrite mono_list_auth_dfrac_op //. Qed.
 
   (** * Validity *)
   Lemma mono_list_auth_dfrac_validN n dq l : ✓{n} (●ML{dq} l) ↔ ✓ dq.
diff --git a/iris/algebra/lib/mono_nat.v b/iris/algebra/lib/mono_nat.v
index 4c562117f..eb437971c 100644
--- a/iris/algebra/lib/mono_nat.v
+++ b/iris/algebra/lib/mono_nat.v
@@ -55,10 +55,10 @@ Section mono_nat.
 
   Global Instance mono_nat_auth_dfrac_is_op dq dq1 dq2 n :
     IsOp dq dq1 dq2 → IsOp' (●MN{dq} n) (●MN{dq1} n) (●MN{dq2} n).
-  Proof. rewrite /IsOp' /IsOp=>->. rewrite mono_nat_auth_dfrac_op //. Qed.
+  Proof. rewrite /IsOp' /IsOp=> ->. rewrite mono_nat_auth_dfrac_op //. Qed.
   Global Instance mono_nat_lb_max_is_op n n1 n2 :
     IsOp (MaxNat n) (MaxNat n1) (MaxNat n2) → IsOp' (◯MN n) (◯MN n1) (◯MN n2).
-  Proof. rewrite /IsOp' /IsOp /mono_nat_lb=>->. done. Qed.
+  Proof. rewrite /IsOp' /IsOp /mono_nat_lb=> ->. done. Qed.
 
   (** rephrasing of [mono_nat_lb_op] useful for weakening a fragment to a
   smaller lower-bound *)
-- 
GitLab