From eb203c6b6e11862d7f3b60d6d8e4b2377c25be7b Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 18 Dec 2017 19:53:53 +0100
Subject: [PATCH] Tweak.

---
 theories/bi/monpred.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index d3fad5485..b98c092bb 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -500,7 +500,7 @@ Global Instance monPred_car_timeless P i : Timeless P → Timeless (P i).
 Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed.
 Global Instance monPred_ipure_timeless (P : PROP) :
   Timeless P → @Timeless (monPredSI I PROP) ⎡P⎤%I.
-Proof. intros. split => ? /=. unseal. exact: H. Qed.
+Proof. intros. split => ? /=. by unseal. Qed.
 Global Instance monPred_in_timeless i0 : Timeless (@monPred_in I PROP i0).
 Proof. split => ? /=. unseal. apply timeless, _. Qed.
 Global Instance monPred_all_timeless P :
-- 
GitLab