diff --git a/algebra/cmra.v b/algebra/cmra.v
index 94a6e73c1c96200567d34c7f6285d86f165475bc..934b59a5d10d952dbbf2250a57b9c574422a96f0 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -11,7 +11,7 @@ Notation "(â‹…)" := op (only parsing) : C_scope.
 Definition included `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
 Infix "≼" := included (at level 70) : C_scope.
 Notation "(≼)" := included (only parsing) : C_scope.
-Hint Extern 0 (?x ≼ ?y) => reflexivity.
+Hint Extern 0 (_ ≼ _) => reflexivity.
 Instance: Params (@included) 3.
 
 Class Minus (A : Type) := minus : A → A → A.
@@ -32,7 +32,7 @@ Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x
 Notation "x ≼{ n } y" := (includedN n x y)
   (at level 70, format "x  ≼{ n }  y") : C_scope.
 Instance: Params (@includedN) 4.
-Hint Extern 0 (?x ≼{_} ?y) => reflexivity.
+Hint Extern 0 (_ ≼{_} _) => reflexivity.
 
 Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := {
   (* setoids *)
diff --git a/algebra/cofe.v b/algebra/cofe.v
index 1b77fde092ace5d3e14994817349dd2e0564b2c1..6d318ba4feb5429c0a474dedba8d8e53b14dc997 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -5,7 +5,7 @@ Class Dist A := dist : nat → relation A.
 Instance: Params (@dist) 3.
 Notation "x ≡{ n }≡ y" := (dist n x y)
   (at level 70, n at next level, format "x  ≡{ n }≡  y").
-Hint Extern 0 (?x ≡{_}≡ ?y) => reflexivity.
+Hint Extern 0 (_ ≡{_}≡ _) => reflexivity.
 Hint Extern 0 (_ ≡{_}≡ _) => symmetry; assumption.
 
 Tactic Notation "cofe_subst" ident(x) :=
diff --git a/algebra/upred.v b/algebra/upred.v
index c4f712575c8eb627d917618ae5660402120c0b7c..6a44e866ef17c08fefbcbf70f75eac0a05fa0ac5 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -97,7 +97,7 @@ Qed.
 
 (** logical entailement *)
 Definition uPred_entails {M} (P Q : uPred M) := ∀ x n, ✓{n} x → P n x → Q n x.
-Hint Extern 0 (uPred_entails ?P ?P) => reflexivity.
+Hint Extern 0 (uPred_entails _ _) => reflexivity.
 Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
 
 (** logical connectives *)
diff --git a/prelude/base.v b/prelude/base.v
index 3f30a1122c5cd19255ebdd8cf3bb02011c9e0252..f711649e7014bff9f132e3546a9b6df8753e904a 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -53,7 +53,7 @@ Notation "(≠)" := (λ x y, x ≠ y) (only parsing) : C_scope.
 Notation "( x ≠)" := (λ y, x ≠ y) (only parsing) : C_scope.
 Notation "(≠ x )" := (λ y, y ≠ x) (only parsing) : C_scope.
 
-Hint Extern 0 (?x = ?x) => reflexivity.
+Hint Extern 0 (_ = _) => reflexivity.
 Hint Extern 100 (_ ≠ _) => discriminate.
 
 Notation "(→)" := (λ A B, A → B) (only parsing) : C_scope.
@@ -198,7 +198,7 @@ Instance: Params (@equiv) 2.
 (for types that have an [Equiv] instance) rather than the standard Leibniz
 equality. *)
 Instance equiv_default_relation `{Equiv A} : DefaultRelation (≡) | 3.
-Hint Extern 0 (?x ≡ ?y) => reflexivity.
+Hint Extern 0 (_ ≡ _) => reflexivity.
 Hint Extern 0 (_ ≡ _) => symmetry; assumption.
 
 (** ** Operations on collections *)
diff --git a/prelude/list.v b/prelude/list.v
index d0e0eafb0b74e606bcc6a212063f8e12f481c750..34645eeb4909690a848d83e13bfa71310b0250c0 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -220,8 +220,8 @@ Definition suffix_of {A} : relation (list A) := λ l1 l2, ∃ k, l2 = k ++ l1.
 Definition prefix_of {A} : relation (list A) := λ l1 l2, ∃ k, l2 = l1 ++ k.
 Infix "`suffix_of`" := suffix_of (at level 70) : C_scope.
 Infix "`prefix_of`" := prefix_of (at level 70) : C_scope.
-Hint Extern 0 (?x `prefix_of` ?y) => reflexivity.
-Hint Extern 0 (?x `suffix_of` ?y) => reflexivity.
+Hint Extern 0 (_ `prefix_of` _) => reflexivity.
+Hint Extern 0 (_ `suffix_of` _) => reflexivity.
 
 Section prefix_suffix_ops.
   Context `{∀ x y : A, Decision (x = y)}.
@@ -249,7 +249,7 @@ Inductive sublist {A} : relation (list A) :=
   | sublist_skip x l1 l2 : sublist l1 l2 → sublist (x :: l1) (x :: l2)
   | sublist_cons x l1 l2 : sublist l1 l2 → sublist l1 (x :: l2).
 Infix "`sublist`" := sublist (at level 70) : C_scope.
-Hint Extern 0 (?x `sublist` ?y) => reflexivity.
+Hint Extern 0 (_ `sublist` _) => reflexivity.
 
 (** A list [l2] contains a list [l1] if [l2] is obtained by removing elements
 from [l1] while possiblity changing the order. *)
@@ -260,7 +260,7 @@ Inductive contains {A} : relation (list A) :=
   | contains_cons x l1 l2 : contains l1 l2 → contains l1 (x :: l2)
   | contains_trans l1 l2 l3 : contains l1 l2 → contains l2 l3 → contains l1 l3.
 Infix "`contains`" := contains (at level 70) : C_scope.
-Hint Extern 0 (?x `contains` ?y) => reflexivity.
+Hint Extern 0 (_ `contains` _) => reflexivity.
 
 Section contains_dec_help.
   Context {A} {dec : ∀ x y : A, Decision (x = y)}.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 0eb96eadb3d4edc37e9747ec0e4b5d7024aaf21d..db9e9ccd3705fa29423e543aff53ba0e2812c76b 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -86,9 +86,6 @@ Qed.
 Lemma vs_mask_frame' E Ef P Q : Ef ∩ E = ∅ → (P ={E}=> Q) ⊑ (P ={E ∪ Ef}=> Q).
 Proof. intros; apply vs_mask_frame; solve_elem_of. Qed.
 
-(* FIXME: This is needed to make eauto solve [inv N R ⊑ inv N ?c]. *)
-Local Hint Extern 100 (_ ⊑ _) => reflexivity.
-
 Lemma vs_open_close N E P Q R :
   nclose N ⊆ E →
   (inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊑ (P ={E}=> Q).