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.

1 files changed, 32 insertions, 4 deletions

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.