From 94d26232844ffbfcf32f01e2e00abfc468b392ec Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Mon, 7 Dec 2020 21:22:35 +0100
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)

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

diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index ea4b589ed..a8e7b420d 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -52,7 +52,7 @@ Definition wp_pre `{!irisG Λ Σ} (s : stuckness)
 
 Local Instance wp_pre_contractive `{!irisG Λ Σ} s : Contractive (wp_pre s).
 Proof.
-  rewrite /wp_pre /==> n wp wp' Hwp E e1 Φ.
+  rewrite /wp_pre /= => n wp wp' Hwp E e1 Φ.
   repeat (f_contractive || f_equiv); apply Hwp.
 Qed.
 
-- 
GitLab