From 6231b7b9dd91575143f3b7faac399ad531cee522 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 6 Nov 2019 20:23:36 +0100
Subject: [PATCH] Stylistic tweaks in `monPred`.

---
 theories/bi/monpred.v | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 95394a06b..6a4e99370 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -447,13 +447,10 @@ Proof. move => [] /(_ i). unfold Absorbing. by unseal. Qed.
 Global Instance monPred_at_affine P i : Affine P → Affine (P i).
 Proof. move => [] /(_ i). unfold Affine. by unseal. Qed.
 
-(* Note that monPred_in is *not* Plain, because it does depend on the
-   index. *)
-Global Instance monPred_in_persistent i :
-  Persistent (@monPred_in I PROP i).
+(** Note that [monPred_in] is *not* [Plain], because it depends on the index. *)
+Global Instance monPred_in_persistent i : Persistent (@monPred_in I PROP i).
 Proof. unfold Persistent. unseal; split => ?. by apply bi.pure_persistent. Qed.
-Global Instance monPred_in_absorbing i :
-  Absorbing (@monPred_in I PROP i).
+Global Instance monPred_in_absorbing i : Absorbing (@monPred_in I PROP i).
 Proof. unfold Absorbing. unseal. split=> ? /=. apply absorbing, _. Qed.
 
 Definition monPred_embedding_mixin : BiEmbedMixin PROP monPredI monPred_embed.
-- 
GitLab