From ee6743d2879d874cad13bd05b5be3847ac27062e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 28 Aug 2014 16:45:10 +0200
Subject: Fixing an unnatural selection of subterms larger than expected in the
 presence of let-ins.

---
 test-suite/success/destruct.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 4a7657e292..48927b6cc3 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.
-- 
cgit v1.2.3