1 files changed, 85 insertions, 0 deletions
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
new file mode 100644
index 00000000..a9e4a843
--- /dev/null
+++ b/test-suite/success/Inversion.v
@@ -0,0 +1,85 @@
+Axiom magic:False.
+
+(* Submitted by Dachuan Yu (bug #220) *)
+Fixpoint T[n:nat] : Type := 
+ Cases n of 
+ | O => (nat -> Prop) 
+ | (S n') => (T n') 
+ end. 
+Inductive R : (n:nat)(T n) -> nat -> Prop := 
+  | RO : (Psi:(T O); l:nat) 
+          (Psi l) -> (R O Psi l) 
+  | RS : (n:nat; Psi:(T (S n)); l:nat) 
+          (R n Psi l) -> (R (S n) Psi l). 
+Definition Psi00 : (nat -> Prop) := [n:nat] False. 
+Definition Psi0 : (T O) := Psi00. 
+Lemma Inversion_RO : (l:nat)(R O Psi0 l) -> (Psi00 l).
+Inversion 1.
+Abort.
+
+(* Submitted by Pierre Casteran (bug #540) *)
+
+Set Implicit Arguments.
+Parameter rule: Set -> Type.
+
+Inductive extension [I:Set]:Type :=
+ NL : (extension I) 
+|add_rule : (rule I)  -> (extension I)  -> (extension I).
+
+
+Inductive in_extension [I :Set;r: (rule I)] : (extension I)  -> Type :=
+ in_first : (e:?)(in_extension r (add_rule r e))
+|in_rest : (e,r':?)(in_extension r e) -> (in_extension r (add_rule r' e)).
+
+Implicits NL [1].
+
+Inductive super_extension [I:Set;e :(extension I)] : (extension I)  -> Type :=
+ super_NL   : (super_extension   e NL)
+| super_add : (r:?)(e': (extension I))
+                 (in_extension  r e) ->
+                 (super_extension  e e') ->
+                 (super_extension  e (add_rule r e')). 
+
+
+
+Lemma super_def : (I :Set)(e1, e2: (extension I))
+                 (super_extension  e2 e1) ->
+                 (ru:?) 
+                   (in_extension ru e1) ->
+                   (in_extension ru e2).
+Proof.                 
+ Induction 1.
+ Inversion 1; Auto.
+ Elim magic.
+Qed.
+
+(* Example from Norbert Schirmer on Coq-Club, Sep 2000 *)
+
+Unset Implicit Arguments.
+Definition Q[n,m:nat;prf:(le n m)]:=True.
+Goal (n,m:nat;H:(le (S n) m))(Q (S n) m H)==True.
+Intros.
+Dependent Inversion_clear H.
+Elim magic.
+Elim magic.
+Qed.
+
+(* Submitted by Boris Yakobowski (bug #529) *)
+(* Check that Inversion does not fail due to unnormalized evars *)
+
+Set Implicit Arguments.
+Require Import Bvector.
+
+Inductive I : nat -> Set :=
+| C1 : (I (S O))
+| C2 : (k,i:nat)(vector (I i) k) -> (I i).
+
+Inductive SI : (k:nat)(I k) -> (vector nat k) -> nat -> Prop :=
+| SC2 : (k,i,vf:nat) (v:(vector (I i) k))(xi:(vector nat i))(SI (C2 v) xi vf).
+
+Theorem SUnique : (k:nat)(f:(I k))(c:(vector nat k))
+(v,v':?) (SI f c v) -> (SI f c v') -> v=v'.
+Proof.
+NewInduction 1.
+Intros H ; Inversion H.
+Admitted.