From 613168bf8af3af0fe31873efd89038a89800792e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 10 Feb 2017 11:51:19 +0100
Subject: [PATCH] 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   | 5 +++++
 theories/coPset.v | 2 +-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/theories/base.v b/theories/base.v
index 65233ddf..7b5ae81c 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 4536fc96..a848f5c8 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.
 
-- 
GitLab