From b6ad586875856117b1b9938cd7317e582f0d96b9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 21 Aug 2013 14:44:33 +0200
Subject: [PATCH] Make arguments of proj1_sig maximally implicit.

---
 theories/assoc.v | 3 +--
 theories/base.v  | 3 ++-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/assoc.v b/theories/assoc.v
index bfd254d0..f6303ac4 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 f4af422b..f4d1e2ce 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 *)
-- 
GitLab