From 2b31c2a5dfcf091e74e2df41c1504c932e0f044e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 20 Mar 2005 11:24:07 +0000
Subject: Test d'un bug de 'Inv.dependent_hyps' qui ne met pas à jour le type
 des hyps dépendantes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6867 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/Inversion.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index a9e4a8434a..40d45afdee 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -83,3 +83,13 @@ Proof.
 NewInduction 1.
 Intros H ; Inversion H.
 Admitted.
+
+(* Used to failed at some time *)
+
+Parameter bar : (p,q:nat) p=q -> Prop.
+Inductive foo : nat -> nat -> Prop := 
+  C : (a,b:nat)(Heq:a = b) (bar a b Heq) -> (foo a b).
+Lemma depinv : (a,b:?) (foo a b) -> True.
+Intros a b H.
+Inversion H.
+Abort.
-- 
cgit v1.2.3