From cc27d50bf7423fe1df00330eddcd81d18b55fd0f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 30 Oct 2014 15:52:13 +0100
Subject: Enlarge the cases where the like first selection is used in destruct.

This is now a "like first" strategy iff there is no occurrences
selected in either the goal or in one of the hypotheses possibly given
in an "in" clause. Before, it was "like first" if and only if no "in"
clause was given at all.
---
 test-suite/success/destruct.v | 36 ++++++++++++++++++++++++++++++++----
 1 file changed, 32 insertions(+), 4 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 56ec6a02d6..5f94d8e722 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -256,9 +256,9 @@ Qed.
 (* Check destruct on idents with maximal implicit arguments - which did
    not work in 8.4 *)
 
-Parameter f : forall {n:nat}, n=n -> nat.
-Goal f (eq_refl 0) = 0.
-destruct f.
+Parameter g : forall {n:nat}, n=n -> nat.
+Goal g (eq_refl 0) = 0.
+destruct g.
 Abort.
 
 (* This one was working in 8.4 (because of full conv on closed arguments) *)
@@ -278,7 +278,7 @@ Goal forall f : A -> nat -> nat, f a 0 = f a 1.
 intros.
 destruct f.
 
-(* This one was not working in 8.4 *)
+(* This was not working in 8.4 *)
 
 Section S1.
 Variables x y : Type.
@@ -290,6 +290,34 @@ change (x=y) in H.
 Abort.
 End S1.
 
+(* This was not working in 8.4 *)
+
+Goal forall g:nat->nat, g 0 = g 1 -> g 1 = g 2 -> g 0 = g 2.
+intros.
+induction g.
+2:change (n = g 1 -> n = g 2) in IHn.
+Abort.
+
+(* This was not working in 8.4 *)
+
+Goal forall g:nat->nat, g 0 = g 1 -> g 1 = g 2 -> g 0 = g 2. 
+intros g H H0.
+induction g in H |- *.
+Abort.
+
+(* "at" was not granted in 8.4 in the next two examples *)
+
+Goal forall g:nat->nat, g 0 = g 1 -> g 1 = g 2 -> g 0 = g 2. 
+intros g H H0.
+induction g in H at 2, H0 at 1.
+change (g 0 = 0) in H.
+Abort.
+
+Goal forall g:nat->nat, g 0 = g 1 -> g 1 = g 2 -> g 0 = g 2. 
+intros g H H0.
+Fail induction g in H at 2 |- *. (* Incompatible occurrences *)
+Abort.
+
 (* These ones are not satisfactory at the current time
 
 Section S2.
-- 
cgit v1.2.3