From d6c7bf2ec750876c9b35ee9d84840f2ab643dbfe Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 21 Nov 2013 18:39:22 -0500
Subject: Better unification for [projT1] and [proj1_sig].

This way, [fun A (P : A -> Prop) (X : sigT P) => proj1_sig X] unifies
with [fun A (P : A -> Prop) (X : sigT P) => projT1 X].

This closes Bug 3043.
---
 test-suite/bugs/closed/3043.v | 3 +++
 theories/Init/Specif.v        | 8 ++++----
 2 files changed, 7 insertions(+), 4 deletions(-)
 create mode 100644 test-suite/bugs/closed/3043.v

diff --git a/test-suite/bugs/closed/3043.v b/test-suite/bugs/closed/3043.v
new file mode 100644
index 0000000000..12885987f8
--- /dev/null
+++ b/test-suite/bugs/closed/3043.v
@@ -0,0 +1,3 @@
+Goal (fun A (P : A -> Prop) (X : sigT P) => proj1_sig X) = (fun A (P : A -> Prop) (X : sigT P) => projT1 X).
+  reflexivity.
+Qed.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 88c2c264ad..ee81116399 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -107,11 +107,11 @@ End Projections.
 
 (** [sigT] of a predicate is equivalent to [sig] *)
 
-Lemma sig_of_sigT : forall (A:Type) (P:A->Prop), sigT P -> sig P.
-Proof. destruct 1 as (x,H); exists x; trivial. Defined.
+Definition sig_of_sigT (A : Type) (P : A -> Prop) (X : sigT P) : sig P
+  := exist P (projT1 X) (projT2 X).
 
-Lemma sigT_of_sig : forall (A:Type) (P:A->Prop), sig P -> sigT P.
-Proof. destruct 1 as (x,H); exists x; trivial. Defined.
+Definition sigT_of_sig (A : Type) (P : A -> Prop) (X : sig P) : sigT P
+  := existT P (proj1_sig X) (proj2_sig X).
 
 Coercion sigT_of_sig : sig >-> sigT.
 Coercion sig_of_sigT : sigT >-> sig.
-- 
cgit v1.2.3