diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-28 12:37:43 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-28 19:55:01 +0200 |
| commit | 469c5bfc849e06d5a32d7aaabdf9b2fa3f451f4a (patch) | |
| tree | b227dd4e28501b2c325a99711fb4c659a6ac6ba2 /test-suite/bugs/closed/3546.v | |
| parent | 3fdfb3ccb7986b1e4c7685b440a62730107a639f (diff) | |
Fix bugs #3484 and #3546.
The unification oracle now prefers unfolding the eta-expanded form of a
projection over the primitive projection, and allows first-order
unification on applications of constructors of primitive records,
in case eta-conversion fails (disabled by previous patch on eta).
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 000000000..55d718bd0 --- /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)". + *) |