diff options
| author |  Jason Gross <jgross@mit.edu> | 2013-11-21 18:42:43 -0500 |
|---|---|---|
| committer |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-04-10 15:05:13 +0200 |
| commit | f705a0b0ae587e323199c43e9669b4f96adf4d77 (patch) | |
| tree | 08af2d10889d5bbe5593a61241d9e3a70d2b150e /test-suite/bugs/closed | |
| parent | ff8bac52149f8a32498f765bd579e00fcbd4f080 (diff) | |
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.
Diffstat (limited to 'test-suite/bugs/closed')
| -rw-r--r-- | test-suite/bugs/closed/3044.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3044.v b/test-suite/bugs/closed/3044.v new file mode 100644 index 000000000..2e6fd6ad2 --- /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. |