Ajout bug #540

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5452 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 34 insertions, 0 deletions

diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index c28e04eb71..636540fbd7 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -14,3 +14,37 @@ 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.