From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 test-suite/success/Inversion.v | 36 +++++++++++++++++++++++++++++-------
 1 file changed, 29 insertions(+), 7 deletions(-)

(limited to 'test-suite/success/Inversion.v')

diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index b08ffcc3..5091b44c 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -5,13 +5,13 @@ Fixpoint T (n : nat) : Type :=
   match n with
   | O => nat -> Prop
   | S n' => T n'
-  end. 
+  end.
 Inductive R : forall n : nat, T n -> nat -> Prop :=
   | RO : forall (Psi : T 0) (l : nat), Psi l -> R 0 Psi l
   | RS :
-      forall (n : nat) (Psi : T (S n)) (l : nat), R n Psi l -> R (S n) Psi l. 
-Definition Psi00 (n : nat) : Prop := False. 
-Definition Psi0 : T 0 := Psi00. 
+      forall (n : nat) (Psi : T (S n)) (l : nat), R n Psi l -> R (S n) Psi l.
+Definition Psi00 (n : nat) : Prop := False.
+Definition Psi0 : T 0 := Psi00.
 Lemma Inversion_RO : forall l : nat, R 0 Psi0 l -> Psi00 l.
 inversion 1.
 Abort.
@@ -39,14 +39,14 @@ extension I -> Type :=
   | super_add :
       forall r (e' : extension I),
       in_extension r e ->
-      super_extension e e' -> super_extension e (add_rule r e'). 
+      super_extension e e' -> super_extension e (add_rule r e').
 
 
 
 Lemma super_def :
  forall (I : Set) (e1 e2 : extension I),
  super_extension e2 e1 -> forall ru, in_extension ru e1 -> in_extension ru e2.
-Proof.                 
+Proof.
  simple induction 1.
  inversion 1; auto.
  elim magic.
@@ -105,5 +105,27 @@ Abort.
 Inductive foo2 : option nat -> Prop := Foo : forall t, foo2 (Some t).
 Goal forall o, foo2 o -> 0 = 1.
 intros.
-eapply trans_eq. 
+eapply trans_eq.
 inversion H.
+
+(* Check that the part of "injection" that is called by "inversion"
+   does the same number of intros as the number of equations
+   introduced, even in presence of dependent equalities that
+   "injection" renounces to split *)
+
+Fixpoint prodn (n : nat) :=
+  match n with
+  | O => unit
+  | (S m) => prod (prodn m) nat
+  end.
+
+Inductive U : forall n : nat, prodn n -> bool -> Prop :=
+| U_intro : U 0 tt true.
+
+Lemma foo3 : forall n (t : prodn n), U n t true -> False.
+Proof.
+(* used to fail because dEqThen thought there were 2 new equations but
+   inject_at_positions actually introduced only one; leading then to
+   an inconsistent state that disturbed "inversion" *)
+intros. inversion H.
+Abort.
-- 
cgit v1.2.3