From 9a508dcc671d70c375fa5745642eab51cc89bb66 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 6 Feb 2004 13:58:13 +0000 Subject: 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 --- test-suite/success/Case15.v | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/test-suite/success/Case15.v b/test-suite/success/Case15.v index 19579d5558..2294452001 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]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]Cases B of - (boite true n) => n -| (boite false (n,m)) => (plus n m) -end. *) -- cgit v1.2.3