Make arguments for sig and sigT constructors and projections maximally implicit.

Some were already maximally implicit, some were not. Now it is consistent.

theories/base.v

@@ -551,7 +551,12 @@ Instance option_inhabited {A} : Inhabited (option A) := populate None.
 
 (** ** Sigma types *)
 Arguments existT {_ _} _ _.
+Arguments projT1 {_ _} _.
+Arguments projT2 {_ _} _.
+
+Arguments exist {_} _ _ _.
 Arguments proj1_sig {_ _} _.
+Arguments proj2_sig {_ _} _.
 Notation "x ↾ p" := (exist _ x p) (at level 20) : C_scope.
 Notation "` x" := (proj1_sig x) (at level 10, format "` x") : C_scope.
 

theories/coPset.v

@@ -186,7 +186,7 @@ Qed.
 Instance coPset_leibniz : LeibnizEquiv coPset.
 Proof.
   intros X Y; rewrite elem_of_equiv; intros HXY.
-  apply (sig_eq_pi _), coPset_eq; try apply proj2_sig.
+  apply (sig_eq_pi _), coPset_eq; try apply @proj2_sig.
   intros p; apply eq_bool_prop_intro, (HXY p).
 Qed.