1 files changed, 14 insertions, 11 deletions
diff --git a/test-suite/success/Case15.v b/test-suite/success/Case15.v
index 22944520..8431880d 100644
--- a/test-suite/success/Case15.v
+++ b/test-suite/success/Case15.v
@@ -2,20 +2,23 @@
    apparently of inductive type *)
 
 (* Check that the non dependency in y is OK both in V7 and V8 *)
-Check ([x;y:Prop;z]<[x][z]x=x \/ z=z>Cases x y z of
-           | O y z' => (or_introl ? (z'=z') (refl_equal ? O))
-           | _ y O => (or_intror ?? (refl_equal ? O))
-           | x y _ => (or_introl ?? (refl_equal ? x))
-           end).
+Check
+  (fun x (y : Prop) z =>
+   match x, y, z return (x = x \/ z = z) with
+   | O, y, z' => or_introl (z' = z') (refl_equal 0)
+   | _, y, O => or_intror _ (refl_equal 0)
+   | 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. 
+Inductive Boite : Set :=
+    boite : forall b : bool, (if b then nat else (nat * nat)%type) -> Boite. 
 
-Definition test := [B:Boite]<nat>Cases B of 
-  (boite true n) => n 
-| (boite false (n,m)) => (plus n m)
-end.
+Definition test (B : Boite) :=
+  match B return nat with
+  | boite true n => n
+  | boite false (n, m) => n + m
+  end.
 
 (* Check lazyness of compilation ... future work
 Inductive I : Set := c : (b:bool)(if b then bool else nat)->I.