From 179e1d5451411f96a5032e244f2f6cd57463e3bd Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 25 Apr 2017 14:09:23 -0400
Subject: Use notation for sigT

---
 theories/Init/Specif.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index e4c57c6c12..771a10531c 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -265,7 +265,7 @@ Section sigT.
       but for simplicity, we don't. *)
   Definition eq_sigT_uncurried_iff {A P}
              (u v : { a : A & P a })
-    : u = v <-> (sigT (fun p : projT1 u = projT1 v => rew p in projT2 u = projT2 v)).
+    : u = v <-> { p : projT1 u = projT1 v & rew p in projT2 u = projT2 v }.
   Proof.
     split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sigT_uncurried ].
   Defined.
-- 
cgit v1.2.3