diff --git a/theories/algebra/deprecated.v b/theories/algebra/deprecated.v
index 3ff595195b3de5228a84d27217d1ae5ea511d319..8a64ae6f854ce5386b31469224f5a6c706806e66 100644
--- a/theories/algebra/deprecated.v
+++ b/theories/algebra/deprecated.v
@@ -50,6 +50,8 @@ Qed.
 Canonical Structure dec_agreeR : cmraT :=
   discreteR (dec_agree A) dec_agree_ra_mixin.
 
+Global Instance dec_agree_cmra_discrete : CMRADiscrete dec_agreeR.
+Proof. apply discrete_cmra_discrete. Qed.
 Global Instance dec_agree_total : CMRATotal dec_agreeR.
 Proof. intros x. by exists x. Qed.
 
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 990410360c0f5a95d51adef8e946bbc386088683..1ce8e901b9dc70ef3a78688adca092ca6d9a5c9d 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 40d4fad4924eade965ce1b53f9f72838615d8699..b44d267e92e58f8a4481670d2699cf57c5d37e0e 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 {_} _ _ {_}.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index a70bacbf2ca8460249ec4ba8c4dad8bd07612cf5..cd4b760209e71798be20077b45ffa79a17f3590e 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -441,7 +441,7 @@ Tactic Notation "iApply" open_constr(lem) :=
       |lazy beta (* reduce betas created by instantiation *)]
     |iSpecializePat H "[]"; last go H] in
   iPoseProofCore lem as false true (fun H =>
-    first [iExact H|go H|iTypeOf H (fun Q => fail 1 "iApply: cannot apply" Q)]).
+    first [iExact H|go H|iTypeOf H (fun _ Q => fail "iApply: cannot apply" Q)]).
 
 (** * Revert *)
 Local Tactic Notation "iForallRevert" ident(x) :=