Commit b6ad5868 authored by Robbert Krebbers's avatar Robbert Krebbers

Make arguments of proj1_sig maximally implicit.

parent 5c785a10
...@@ -240,8 +240,7 @@ Proof. ...@@ -240,8 +240,7 @@ Proof.
induction l2 as [|[??] l2 IH2]; simplify_assoc; rewrite ?IH; simplify_assoc. induction l2 as [|[??] l2 IH2]; simplify_assoc; rewrite ?IH; simplify_assoc.
Qed. Qed.
Global Instance assoc_to_list {A} : FinMapToList K A (assoc K A) := Global Instance assoc_to_list {A} : FinMapToList K A (assoc K A) := proj1_sig.
@proj1_sig _ _.
Lemma assoc_to_list_nodup {A} (l : list (K * A)) : assoc_wf l NoDup l. Lemma assoc_to_list_nodup {A} (l : list (K * A)) : assoc_wf l NoDup l.
Proof. Proof.
revert l. assert ( i x (l : list (K * A)), assoc_before i l (i,x) l). revert l. assert ( i x (l : list (K * A)), assoc_before i l (i,x) l).
......
...@@ -72,8 +72,9 @@ Notation "(↔ B )" := (λ A, A ↔ B) (only parsing) : C_scope. ...@@ -72,8 +72,9 @@ Notation "(↔ B )" := (λ A, A ↔ B) (only parsing) : C_scope.
(** Set convenient implicit arguments for [existT] and introduce notations. *) (** Set convenient implicit arguments for [existT] and introduce notations. *)
Arguments existT {_ _} _ _. Arguments existT {_ _} _ _.
Arguments proj1_sig {_ _} _.
Notation "x ↾ p" := (exist _ x p) (at level 20) : C_scope. 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 *) (** * Type classes *)
(** ** Provable propositions *) (** ** Provable propositions *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment