diff options
| -rw-r--r-- | test-suite/success/Case15.v | 15 |
1 files 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]<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. *) |