From 545eea68d54732f1f76a1a5a5f575d8b1c8ee7df Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 29 May 2018 11:52:47 +0200
Subject: [PATCH] Revert `IntoWand` part of ec4ac846, and associated change in
 9b14f90a.

---
 theories/proofmode/class_instances_bi.v | 12 +++---------
 theories/proofmode/classes.v            |  4 +---
 2 files changed, 4 insertions(+), 12 deletions(-)

diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index d192be06a..3e538bb6f 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -395,15 +395,9 @@ Proof. by rewrite /IntoWand /= intuitionistically_persistently_elim. Qed.
 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⎤ P ⎡QQ⎤.
-Proof.
-  rewrite /IntoEmbed /IntoWand !embed_intuitionistically_if_2=> -> ->.
-  apply bi.wand_intro_l.
-  by rewrite embed_intuitionistically_if_2 -embed_sep bi.wand_elim_r.
-Qed.
+Global Instance into_wand_embed `{BiEmbed PROP PROP'} p q R P Q :
+  IntoWand p q R P Q → IntoWand p q ⎡R⎤ ⎡P⎤ ⎡Q⎤.
+Proof. by rewrite /IntoWand !embed_intuitionistically_if_2 -embed_wand=> ->. Qed.
 
 (* FromWand *)
 Global Instance from_wand_wand P1 P2 : FromWand (P1 -∗ P2) P1 P2.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 5fe9568de..3ead29d0f 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -482,14 +482,12 @@ 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⎤].
-Also used backwards, i.e. Input [Q] and output [P]. *)
+Input: the proposition [P], output: the proposition [Q] so that [P ⊢ ⎡Q⎤]. *)
 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