diff options
Diffstat (limited to 'test-suite/bugs/closed/3546.v')
| -rw-r--r-- | test-suite/bugs/closed/3546.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3546.v b/test-suite/bugs/closed/3546.v new file mode 100644 index 00000000..55d718bd --- /dev/null +++ b/test-suite/bugs/closed/3546.v @@ -0,0 +1,17 @@ +Set Primitive Projections. +Record prod A B := pair { fst : A ; snd : B }. +Arguments pair {_ _} _ _. +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. +Definition ap11 {A B} {f g:A->B} (h:f=g) {x y:A} (p:x=y) : f x = g y. +Admitted. +Goal forall x y z w : Set, (x, y) = (z, w). +Proof. + intros. + apply ap11. (* Toplevel input, characters 21-25: +Error: In environment +x : Set +y : Set +z : Set +w : Set +Unable to unify "?31 ?191 = ?32 ?192" with "(x, y) = (z, w)". + *) |