From facc4127f0d0d4fbe5f2c255e1d9cb63dd48661f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 27 Apr 2017 12:23:14 +0200
Subject: [PATCH] FromPure instance for later, to make iPureIntro/done work on
 laters.

---
 theories/proofmode/class_instances.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index c435191f9..522129ea0 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -124,6 +124,9 @@ Proof.
   rewrite -Hx. apply pure_intro. done.
 Qed.
 
+Global Instance from_pure_later P φ : FromPure P φ → FromPure (▷ P)%I φ.
+Proof. rewrite /FromPure=> ->. apply later_intro. Qed.
+
 (* IntoPersistentP *)
 Global Instance into_persistentP_always_trans P Q :
   IntoPersistentP P Q → IntoPersistentP (□ P) Q | 0.
-- 
GitLab