Ajout filtrage sur motifs dépendants dans des inductifs différents

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

1 files changed, 9 insertions, 6 deletions

diff --git a/test-suite/success/Case15.v b/test-suite/success/Case15.v
index 19579d555..229445200 100644
--- a/test-suite/success/Case15.v
+++ b/test-suite/success/Case15.v
@@ -8,6 +8,15 @@ Check ([x;y:Prop;z]<[x][z]x=x \/ z=z>Cases x y z of
            | x y _ => (or_introl ?? (refl_equal ? x))
            end).
 
+(* Suggested by Pierre Letouzey (PR#207) *)
+Inductive Boite : Set := 
+  boite : (b:bool)(if b then nat else nat*nat)->Boite. 
+
+Definition test := [B:Boite]<nat>Cases B of 
+  (boite true n) => n 
+| (boite false (n,m)) => (plus n m)
+end.
+
 (* Check lazyness of compilation ... future work
 Inductive I : Set := c : (b:bool)(if b then bool else nat)->I.
 
@@ -36,10 +45,4 @@ Check
             | (S _) => false
             end y)
    end.
-
-(* Suggested by Pierre Letouzey (PR#207) *)
-Definition test := [B:Boite]<nat>Cases B of 
-  (boite true n) => n 
-| (boite false (n,m)) => (plus n m)
-end.
 *)