diff --git a/theories/base.v b/theories/base.v
index 3f30a1122c5cd19255ebdd8cf3bb02011c9e0252..f711649e7014bff9f132e3546a9b6df8753e904a 100644
--- a/theories/base.v
+++ b/theories/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/theories/list.v b/theories/list.v
index d0e0eafb0b74e606bcc6a212063f8e12f481c750..34645eeb4909690a848d83e13bfa71310b0250c0 100644
--- a/theories/list.v
+++ b/theories/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)}.