From 2cbcc992a6604be186d2ecbbd2003d740d3a2970 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 22 Feb 2017 18:35:08 +0100
Subject: [PATCH] Change Hint Mode for FromAssumption.

There is no need to restrict the type class using Hint Mode, we have
a default instance that will always be used first. In case of evars,
the default instance should apply.

The reason for this change is that `iAssumption` should be able to
prove `H : ?e |- P` and `H : P |- ?e`. The former Hint Mode prevented
it from doing that.
---
 theories/proofmode/class_instances.v | 14 ++++++++------
 theories/proofmode/classes.v         |  4 +++-
 2 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 990410360..1ce8e901b 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -10,16 +10,18 @@ Context {M : ucmraT}.
 Implicit Types P Q R : uPred M.
 
 (* FromAssumption *)
-Global Instance from_assumption_False p P : FromAssumption p False P.
-Proof. destruct p; rewrite /FromAssumption /= ?always_pure; apply False_elim. Qed.
-Global Instance from_assumption_exact p P : FromAssumption p P P.
+Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
 Proof. destruct p; by rewrite /FromAssumption /= ?always_elim. Qed.
-Global Instance from_assumption_always_l p P Q :
-  FromAssumption p P Q → FromAssumption p (□ P) Q.
-Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
+Global Instance from_assumption_False p P : FromAssumption p False P | 1.
+Proof. destruct p; rewrite /FromAssumption /= ?always_pure; apply False_elim. Qed.
+
 Global Instance from_assumption_always_r P Q :
   FromAssumption true P Q → FromAssumption true P (□ Q).
 Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
+
+Global Instance from_assumption_always_l p P Q :
+  FromAssumption p P Q → FromAssumption p (□ P) Q.
+Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
 Global Instance from_assumption_later p P Q :
   FromAssumption p P Q → FromAssumption p P (▷ Q)%I.
 Proof. rewrite /FromAssumption=>->. apply later_intro. Qed.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 40d4fad49..b44d267e9 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -5,7 +5,9 @@ Import uPred.
 Class FromAssumption {M} (p : bool) (P Q : uPred M) :=
   from_assumption : □?p P ⊢ Q.
 Arguments from_assumption {_} _ _ _ {_}.
-Hint Mode FromAssumption + + ! - : typeclass_instances.
+(* No need to restrict Hint Mode, we have a default instance that will always
+be used in case of evars *)
+Hint Mode FromAssumption + + - - : typeclass_instances.
 
 Class IntoPure {M} (P : uPred M) (φ : Prop) := into_pure : P ⊢ ⌜φ⌝.
 Arguments into_pure {_} _ _ {_}.
-- 
GitLab