From dd9875747620b905e7081fb376f571d6f368dfee Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 19 Mar 2018 21:13:59 +0100
Subject: [PATCH] get rid of 2nd into_persistent_intuitionistically instance

---
 theories/proofmode/class_instances.v | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index a271c1fcf..144c0762d 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -210,11 +210,13 @@ Global Instance into_persistent_affinely p P Q :
   IntoPersistent p P Q → IntoPersistent p (<affine> P) Q | 0.
 Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed.
 Global Instance into_persistent_intuitionistically p P Q :
-  IntoPersistent p P Q → IntoPersistent p (□ P) Q | 0.
-Proof. rewrite /IntoPersistent /= =><-. by rewrite intuitionistically_elim. Qed.
-Global Instance into_persistent_intuitionistically2 P Q :
-  IntoPersistent true P Q → IntoPersistent false (□ P) Q | 0.
-Proof. rewrite /IntoPersistent /= =><-. by rewrite intuitionistically_persistently_1. Qed.
+  IntoPersistent true P Q → IntoPersistent p (□ P) Q | 0.
+Proof.
+  rewrite /IntoPersistent /= =><-.
+  destruct p; simpl;
+    eauto using persistently_mono, intuitionistically_elim,
+    intuitionistically_persistently_1.
+Qed.
 Global Instance into_persistent_embed `{BiEmbed PROP PROP'} p P Q :
   IntoPersistent p P Q → IntoPersistent p ⎡P⎤ ⎡Q⎤ | 0.
 Proof.
-- 
GitLab