Ajout bug #255

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

1 files changed, 19 insertions, 0 deletions

diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v
index 0a4b284f9..8c6f31b4c 100644
--- a/test-suite/success/univers.v
+++ b/test-suite/success/univers.v
@@ -17,3 +17,22 @@ Lemma lem3 : (P:Prop)P.
 Intro P ; Pattern P.
 Apply lem2.
 Abort.
+
+(* Check managing of universe constraints in inversion *)
+(* Bug report #855 *)
+
+Inductive dep_eq : (X:Type) X -> X -> Prop :=
+   | intro_eq : (X:Type) (f:X)(dep_eq X f f)
+   | intro_feq : (A:Type) (B:A->Type)
+                 let T = (x:A)(B x) in
+                 (f, g:T) (x:A)
+                 (dep_eq (B x) (f x) (g x)) ->
+                 (dep_eq T f g).
+                                                                                
+Require Import Relations.
+                                                                                
+Theorem dep_eq_trans : (X:Type) (transitive X (dep_eq X)).
+Proof.
+  Unfold transitive.
+  Intros X f g h H1 H2.
+  Inversion H1.