diff options
Diffstat (limited to 'test-suite')
| -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 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. |