diff options
author | 2013-11-21 18:39:22 -0500 | |
---|---|---|
committer | 2013-12-12 10:09:50 +0100 | |
commit | d6c7bf2ec750876c9b35ee9d84840f2ab643dbfe (patch) | |
tree | 068e6539f8c9ca5569e2d50a883995d9b6703ed9 /test-suite/bugs/closed/3043.v | |
parent | a9507f72ffb5cb0b594b097c8d1ed137399fca4a (diff) |
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.
Diffstat (limited to 'test-suite/bugs/closed/3043.v')
-rw-r--r-- | test-suite/bugs/closed/3043.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3043.v b/test-suite/bugs/closed/3043.v new file mode 100644 index 000000000..12885987f --- /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. |