From f987ca782d1301d319cf6c4ba8e2ab449ebe903a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 7 Apr 2017 21:03:18 +0200
Subject: [PATCH] Let iSpecialize with a hypotheses behave like iAssumption.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

For example, when having `H : ▷ P → Q` and `HP : P`, we can now
do `iSpecialize ("H" with "HP")`. This is achieved by putting a
`FromAssumption` premise in the base instance for `IntoWand`.
---
 theories/proofmode/class_instances.v | 5 +++--
 theories/proofmode/classes.v         | 2 --
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index b5176725d..a2926d819 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -248,8 +248,9 @@ Global Instance from_later_exist {A} n (Φ Ψ : A → uPred M) :
 Proof. intros ?. rewrite /FromLaterN laterN_exist=> ?. by apply exist_mono. Qed.
 
 (* IntoWand *)
-Global Instance wand_weaken_exact P Q : WandWeaken P Q P Q.
-Proof. done. Qed.
+Global Instance wand_weaken_assumption P1 P2 Q :
+  FromAssumption false P2 P1 → WandWeaken P1 Q P2 Q | 0.
+Proof. by rewrite /WandWeaken /FromAssumption /= =>->. Qed.
 Global Instance wand_weaken_later P Q P' Q' :
   WandWeaken P Q P' Q' → WandWeaken' P Q (▷ P') (▷ Q').
 Proof.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index e44f27ce3..3b82f5140 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -78,8 +78,6 @@ Class WandWeaken' {M} (P Q P' Q' : uPred M) :=
   wand_weaken' :> WandWeaken P Q P' Q'.
 Hint Mode WandWeaken' + - - ! - : typeclass_instances.
 Hint Mode WandWeaken' + - - - ! : typeclass_instances.
-Instance wand_weaken_exact {M} (P Q : uPred M) : WandWeaken P Q P Q | 1000.
-Proof. done. Qed.
 
 Class IntoWand {M} (R P Q : uPred M) := into_wand : R ⊢ P -∗ Q.
 Arguments into_wand {_} _ _ _ {_}.
-- 
GitLab