From f705a0b0ae587e323199c43e9669b4f96adf4d77 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 21 Nov 2013 18:42:43 -0500
Subject: Define [projT3] and [proj3_sig]

Also allow [projT1]/[projT2] to work for [sigT2]s and
[proj1_sig]/[proj2_sig] to work for [sig2]s, by means of coercions.

This closes Bug 3044.
This closes Pull Request #4.
---
 test-suite/bugs/closed/3044.v | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/bugs/closed/3044.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3044.v b/test-suite/bugs/closed/3044.v
new file mode 100644
index 0000000000..2e6fd6ad29
--- /dev/null
+++ b/test-suite/bugs/closed/3044.v
@@ -0,0 +1,11 @@
+Goal (fun A (P Q : A -> Prop) (X : sigT2 P Q) => proj1_sig X) = (fun A (P Q : A -> Prop) (X : sigT2 P Q) => projT1 X).
+  reflexivity.
+Qed.
+
+Goal (fun A (P Q : A -> Prop) (X : sigT2 P Q) => proj2_sig X) = (fun A (P Q : A -> Prop) (X : sigT2 P Q) => projT2 X).
+  reflexivity.
+Qed.
+
+Goal (fun A (P Q : A -> Prop) (X : sigT2 P Q) => proj3_sig X) = (fun A (P Q : A -> Prop) (X : sigT2 P Q) => projT3 X).
+  reflexivity.
+Qed.
-- 
cgit v1.2.3