diff --git a/theories/base.v b/theories/base.v
index 65233ddfe3a3be343c6437f242577bc10dbd6936..7b5ae81c80bc5ae7ce2c5b53fa22ae3193312976 100644
--- a/theories/base.v
+++ b/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.
 
diff --git a/theories/coPset.v b/theories/coPset.v
index 4536fc96eebb147b83cdf04a659b30f1ba348e6e..a848f5c86b0c0e8769c6bf698e6f3743eae786ce 100644
--- a/theories/coPset.v
+++ b/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.