From 861490f06b09c0fc99dfbb8199554465ca99cc91 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 20 Mar 2018 13:49:04 +0100
Subject: [PATCH] FromAffinely instance for intuitionistic modality

---
 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 20f14095d..c01ce3b53 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -13,6 +13,9 @@ Global Instance from_affinely_affine P : Affine P → FromAffinely P P.
 Proof. intros. by rewrite /FromAffinely affinely_elim. Qed.
 Global Instance from_affinely_default P : FromAffinely (<affine> P) P | 100.
 Proof. by rewrite /FromAffinely. Qed.
+Global Instance from_affinely_intuitionistically P :
+  FromAffinely (â–¡ P) (<pers> P) | 100.
+Proof. by rewrite /FromAffinely. Qed.
 
 (* IntoAbsorbingly *)
 Global Instance into_absorbingly_True : @IntoAbsorbingly PROP True emp | 0.
-- 
GitLab