diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-06-23 16:59:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-06-23 19:09:11 +0200 |
| commit | f39a711555d76926b6e0ddf5480a6411abc862a9 (patch) | |
| tree | 51d3f2ae8c87129966cd75919201224f11b61999 /test-suite/success/simpl.v | |
| parent | 47860acaffe6017c3b5165d6442f9fbf5c524495 (diff) | |
Fixing incompatibility introduced with simpl in commit 364decf59c1 (or
maybe ca71714).
Goal 2=2+2.
match goal with |- (_ = ?c) => simpl c end.
was working in 8.4 but was failing in 8.5beta2.
Note: Changes in tacintern.ml are otherwise purely cosmetic.
Diffstat (limited to 'test-suite/success/simpl.v')
| -rw-r--r-- | test-suite/success/simpl.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v index e540ae5f3..5b87e877b 100644 --- a/test-suite/success/simpl.v +++ b/test-suite/success/simpl.v @@ -98,3 +98,10 @@ Fail simpl (unbox _ (unbox _ _)) at 3 4. (* Nested and even overlapping *) simpl (unbox _ (unbox _ _)) at 2 4. match goal with |- unbox _ (Box _ True) = unbox _ (Box _ True) => idtac end. Abort. + +(* Check interpretation of ltac variables (was broken in 8.5 beta 1 and 2 *) + +Goal 2=1+1. +match goal with |- (_ = ?c) => simpl c end. +match goal with |- 2 = 2 => idtac end. (* Check that it reduced *) +Abort. |