1 files changed, 89 insertions, 2 deletions

diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 75643d9d..7ae60d98 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -25,7 +25,7 @@ Check
  fun (P : forall A : Type, let B := A in A -> Type) (f : P True I) (A : Type) =>
    let B := A in
      fun (a : A) (e : eq1 A a) =>
-       match e in (eq1 A0 B0 a0) return (P A0 a0) with
+       match e in (eq1 A0 a0) return (P A0 a0) with
        | refl1 => f
        end.
 
@@ -64,3 +64,90 @@ Undo 2.
 Fail induction (S _) in |- * at 4.
 Abort.
 
+(* Check use of "as" clause *)
+
+Inductive I := C : forall x, x<0 -> I -> I.
+
+Goal forall x:I, x=x.
+intros.
+induction x as [y * IHx].
+change (x = x) in IHx. (* We should have IHx:x=x *)
+Abort.
+
+(* This was not working in 8.4 *)
+
+Goal forall h:nat->nat, h 0 = h 1 -> h 1 = h 2 -> h 0 = h 2.
+intros.
+induction h.
+2:change (n = h 1 -> n = h 2) in IHn.
+Abort.
+
+(* This was not working in 8.4 *)
+
+Goal forall h:nat->nat, h 0 = h 1 -> h 1 = h 2 -> h 0 = h 2. 
+intros h H H0.
+induction h in H |- *.
+Abort.
+
+(* "at" was not granted in 8.4 in the next two examples *)
+
+Goal forall h:nat->nat, h 0 = h 1 -> h 1 = h 2 -> h 0 = h 2. 
+intros h H H0.
+induction h in H at 2, H0 at 1.
+change (h 0 = 0) in H.
+Abort.
+
+Goal forall h:nat->nat, h 0 = h 1 -> h 1 = h 2 -> h 0 = h 2. 
+intros h H H0.
+Fail induction h in H at 2 |- *. (* Incompatible occurrences *)
+Abort.
+
+(* Check generalization with dependencies in section variables *)
+
+Section S3.
+Variables x : nat.
+Definition cond := x = x.
+Goal cond -> x = 0.
+intros H.
+induction x as [|n IHn].
+2:change (n = 0) in IHn. (* We don't want a generalization over cond *)
+Abort.
+End S3.
+
+(* These examples show somehow arbitrary choices of generalization wrt
+   to indices, when those indices are not linear. We check here 8.4
+   compatibility: when an index is a subterm of a parameter of the
+   inductive type, it is not generalized. *)
+
+Inductive repr (x:nat) : nat -> Prop := reprc z : repr x z -> repr x z.
+
+Goal forall x, 0 = x -> repr x x -> True.
+intros x H1 H.
+induction H.
+change True in IHrepr.
+Abort.
+
+Goal forall x, 0 = S x -> repr (S x) (S x) -> True.
+intros x H1 H.
+induction H.
+change True in IHrepr.
+Abort.
+
+Inductive repr' (x:nat) : nat -> Prop := reprc' z : repr' x (S z) -> repr' x z.
+
+Goal forall x, 0 = x -> repr' x x -> True.
+intros x H1 H.
+induction H.
+change True in IHrepr'.
+Abort.
+
+(* In this case, generalization was done in 8.4 and we preserve it; this
+   is arbitrary choice  *)
+
+Inductive repr'' : nat -> nat -> Prop := reprc'' x z : repr'' x z -> repr'' x z.
+
+Goal forall x, 0 = x -> repr'' x x -> True.
+intros x H1 H.
+induction H.
+change (0 = z -> True) in IHrepr''.
+Abort.