diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-28 16:45:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-28 17:16:33 +0200 |
| commit | ee6743d2879d874cad13bd05b5be3847ac27062e (patch) | |
| tree | 520640f52b9f9a1e2b594bc2035bad8ad92ef1fb /test-suite/success | |
| parent | 8b1e0f64e3c2ada90452da301dc5a3a10f4983f8 (diff) | |
Fixing an unnatural selection of subterms larger than expected in the
presence of let-ins.
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/destruct.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 4a7657e29..48927b6cc 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -110,3 +110,13 @@ Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n. do 2 eexists. Fail destruct (_, S _). (* Was succeeding at some time in trunk *) Show Proof. + +(* Avoid unnatural selection of a subterm larger than expected *) + +Goal let g := fun x:nat => x in g (S 0) = 0. +intro. +destruct S. +(* Check that it is not the larger subterm "f (S 0)" which is + selected, as it was the case in 8.4 *) +unfold g at 1. +Abort. |