From cfe2139eec1c9123591756995b557a9f702aaa53 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 21 May 2021 12:53:15 +0200
Subject: [PATCH] Nit: Reduce asymmetry

---
 iris/proofmode/class_instances_updates.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
index cf118ab66..34ee47b91 100644
--- a/iris/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -22,7 +22,7 @@ Global Instance from_pure_bupd `{!BiBUpd PROP} a P φ :
 Proof. rewrite /FromPure=> <-. apply bupd_intro. Qed.
 Global Instance from_pure_fupd `{!BiFUpd PROP} a E P φ :
   FromPure a P φ → FromPure a (|={E}=> P) φ.
-Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed.
+Proof. rewrite /FromPure=> <-. apply fupd_intro. Qed.
 
 Global Instance into_wand_bupd `{!BiBUpd PROP} p q R P Q :
   IntoWand false false R P Q → IntoWand p q (|==> R) (|==> P) (|==> Q).
-- 
GitLab