diff --git a/theories/assoc.v b/theories/assoc.v
index bfd254d0580334b72bff3878d4aead4f5358bb57..f6303ac4661dc3e7e3b2486ceebc08fb0923a8a6 100644
--- a/theories/assoc.v
+++ b/theories/assoc.v
@@ -240,8 +240,7 @@ Proof.
     induction l2 as [|[??] l2 IH2]; simplify_assoc; rewrite ?IH; simplify_assoc.
 Qed.
 
-Global Instance assoc_to_list {A} : FinMapToList K A (assoc K A) :=
-  @proj1_sig _ _.
+Global Instance assoc_to_list {A} : FinMapToList K A (assoc K A) := proj1_sig.
 Lemma assoc_to_list_nodup {A} (l : list (K * A)) : assoc_wf l → NoDup l.
 Proof.
   revert l. assert (∀ i x (l : list (K * A)), assoc_before i l → (i,x) ∉ l).
diff --git a/theories/base.v b/theories/base.v
index f4af422b66409df6d6f9348a98507fe84be62850..f4d1e2ce908f110bf7e394ba7eb146119cbab50c 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -72,8 +72,9 @@ Notation "(↔ B )" := (λ A, A ↔ B) (only parsing) : C_scope.
 
 (** Set convenient implicit arguments for [existT] and introduce notations. *)
 Arguments existT {_ _} _ _.
+Arguments proj1_sig {_ _} _.
 Notation "x ↾ p" := (exist _ x p) (at level 20) : C_scope.
-Notation "` x" := (proj1_sig x) : C_scope.
+Notation "` x" := (proj1_sig x) (at level 10, format "` x") : C_scope.
 
 (** * Type classes *)
 (** ** Provable propositions *)