From 92ded048d5adea9b0a39d3c17800acf2bfb18138 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 9 Nov 2019 11:09:01 +0100
Subject: [PATCH] Use proper unification algorithm for `iAssumption` and
 friends.

This fixes some issues in GPS and RustBelt-relaxed, where the old
unification algorithm is now too weak.
---
 theories/proofmode/class_instances_bi.v | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index 7b9c78bd3..b9aeb7523 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -4,6 +4,13 @@ From iris.proofmode Require Import base modality_instances classes ltac_tactics.
 Set Default Proof Using "Type".
 Import bi.
 
+(** The following lemma is not an instance, but defined using a [Hint Extern] to
+enable the better unification algorithm. *)
+Lemma from_assumption_exact {PROP : bi} p (P : PROP) : FromAssumption p P P.
+Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
+Hint Extern 0 (FromAssumption _ _ _) =>
+  notypeclasses refine (from_assumption_exact _ _) : typeclass_instances.
+
 Section bi_instances.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
@@ -59,9 +66,6 @@ Global Instance into_absorbingly_default P : IntoAbsorbingly (<absorb> P) P | 10
 Proof. by rewrite /IntoAbsorbingly. Qed.
 
 (** FromAssumption *)
-Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
-Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
-
 Global Instance from_assumption_persistently_r P Q :
   FromAssumption true P Q → KnownRFromAssumption true P (<pers> Q).
 Proof.
-- 
GitLab