diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-11 15:05:10 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-11 15:21:33 +0200 |
commit | ae5305a4837cce3c7fd61b92ce8110ac66ec2750 (patch) | |
tree | 3026a62e18044a3126521c0c72eefe8304184262 /test-suite/success/ltac.v | |
parent | 2e07ecfce221840047b2f95c93acdb79a4fe0985 (diff) |
Refining 0c320e79ba30 in fixing interpretation of constr under binders
which was broken after it became possible to have binding names
themselves bound to ltac variables (2fcc458af16b).
Interpretation was corrected, but error message was damaged.
Diffstat (limited to 'test-suite/success/ltac.v')
-rw-r--r-- | test-suite/success/ltac.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index f9df021dc..6c4d4ae98 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -306,3 +306,14 @@ let x := ipattern:y in assert (forall x y, x = y + 0). intro. destruct y. (* Check that the name is y here *) Abort. + +(* An example suggested by Jason (see #4317) showing the intended semantics *) +(* Order of binders is reverted because y is just told to depend on x *) + +Goal 1=1. +let T := constr:(fun a b : nat => a) in + lazymatch T with + | (fun x z => ?y) => pose ((fun x x => y) 2 1) + end. +exact (eq_refl n). +Qed. |