From 9b14f90ab3a0985c173ef33476a2c5d14814305c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 29 May 2018 08:40:13 +0200
Subject: [PATCH] fix into_wand for monpred proofmode

---
 tests/proofmode_monpred.v               | 16 ++++++++++++----
 theories/proofmode/class_instances_bi.v |  3 ++-
 theories/proofmode/classes.v            |  4 +++-
 3 files changed, 17 insertions(+), 6 deletions(-)

diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 4a0a99b97..df6964aba 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -91,10 +91,18 @@ Section tests.
     □ P -∗ ⎡◇ 𝓟⎤ -∗ ⎡◇ 𝓠⎤ -∗ ⎡ ◇ (𝓟 ∗ 𝓠) ⎤.
   Proof. iIntros "#H1 H2 H3". iModIntro ⎡ _ ⎤%I. by iSplitL "H2". Qed.
 
-  (* This is a hack to avoid avoid coq bug #5735: sections variables
-     ignore hint modes. So we assume the instances in a way that
-     cannot be used by type class resolution, and then declare the
-     instance. as such. *)
+  Lemma test_into_wand_embed 𝓟 𝓠 :
+    (𝓟 -∗ ◇ 𝓠) →
+    ⎡𝓟⎤ ⊢@{monPredSI} ◇ ⎡𝓠⎤.
+  Proof.
+    iIntros (HPQ) "HP".
+    iMod (HPQ with "[-]") as "$"; last by auto.
+    iAssumption.
+  Qed.
+
+  (* This is a hack to avoid avoid coq bug #5735: sections variables ignore hint
+     modes. So we assume the instances in a way that cannot be used by type
+     class resolution, and then separately declare the instance as such. *)
   Context (FU0 : BiFUpd PROP * unit).
   Instance FU : BiFUpd PROP := fst FU0.
 
diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index 463eceb4d..d192be06a 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -396,8 +396,9 @@ Global Instance into_wand_persistently_false q R P Q :
   Absorbing R → IntoWand false q R P Q → IntoWand false q (<pers> R) P Q.
 Proof. intros ?. by rewrite /IntoWand persistently_elim. Qed.
 Global Instance into_wand_embed `{BiEmbed PROP PROP'} p q (PP QQ RR : PROP) (P : PROP') :
+  IntoWand p q RR PP QQ →
   IntoEmbed P PP →
-  IntoWand p q RR PP QQ → IntoWand p q ⎡RR⎤ P ⎡QQ⎤.
+  IntoWand p q ⎡RR⎤ P ⎡QQ⎤.
 Proof.
   rewrite /IntoEmbed /IntoWand !embed_intuitionistically_if_2=> -> ->.
   apply bi.wand_intro_l.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index e990414e6..5fe9568de 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -482,12 +482,14 @@ Proof. apply _. Qed.
 (** The class [IntoEmbed P Q] is used to transform hypotheses while introducing
 embeddings using [iModIntro].
 
-Input: the proposition [P], output: the proposition [Q] so that [P ⊢ ⎡Q⎤] *)
+Input: the proposition [P], output: the proposition [Q] so that [P ⊢ ⎡Q⎤].
+Also used backwards, i.e. Input [Q] and output [P]. *)
 Class IntoEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP') (Q : PROP) :=
   into_embed : P ⊢ ⎡Q⎤.
 Arguments IntoEmbed {_ _ _} _%I _%I.
 Arguments into_embed {_ _ _} _%I _%I {_}.
 Hint Mode IntoEmbed + + + ! -  : typeclass_instances.
+Hint Mode IntoEmbed + + + - !  : typeclass_instances.
 
 (* We use two type classes for [AsEmpValid], in order to avoid loops in
    typeclass search. Indeed, the [as_emp_valid_embed] instance would try
-- 
GitLab