1 files changed, 39 insertions, 21 deletions
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 87431a75..1adcbd39 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -1,34 +1,52 @@
 (* Check local definitions in context of inductive types *)
-Inductive A [C,D:Prop; E:=C; F:=D; x,y:E->F] : E -> Set :=
-   I : (z:E)(A C D x y z).
+Inductive A (C D : Prop) (E:=C) (F:=D) (x y : E -> F) : E -> Set :=
+    I : forall z : E, A C D x y z.
 
 Check
-   [C,D:Prop; E:=C; F:=D; x,y:(E ->F);
-    P:((c:C)(A C D x y c) ->Type);
-    f:((z:C)(P z (I C D x y z)));
-    y0:C; a:(A C D x y y0)]
-    <[y1:C; a0:(A C D x y y1)](P y1 a0)>Cases a of (I x0) => (f x0) end.
-
-Record B [C,D:Set; E:=C; F:=D; x,y:E->F] : Set := { p : C; q : E }.
+  (fun C D : Prop =>
+   let E := C in
+   let F := D in
+   fun (x y : E -> F) (P : forall c : C, A C D x y c -> Type)
+     (f : forall z : C, P z (I C D x y z)) (y0 : C) 
+     (a : A C D x y y0) =>
+   match a as a0 in (A _ _ _ _ y1) return (P y1 a0) with
+   | I x0 => f x0
+   end).
+
+Record B (C D : Set) (E:=C) (F:=D) (x y : E -> F) : Set :=  {p : C; q : E}.
 
 Check
-   [C,D:Set; E:=C; F:=D; x,y:(E ->F);
-    P:((B C D x y) ->Type);
-    f:((p0,q0:C)(P (Build_B C D x y p0 q0)));
-    b:(B C D x y)]
-    <[b0:(B C D x y)](P b0)>Cases b of (Build_B x0 x1) => (f x0 x1) end.
+  (fun C D : Set =>
+   let E := C in
+   let F := D in
+   fun (x y : E -> F) (P : B C D x y -> Type)
+     (f : forall p0 q0 : C, P (Build_B C D x y p0 q0)) 
+     (b : B C D x y) =>
+   match b as b0 return (P b0) with
+   | Build_B x0 x1 => f x0 x1
+   end).
 
 (* Check implicit parameters of inductive types (submitted by Pierre
   Casteran and also implicit in #338) *)
 
 Set Implicit Arguments.
+Unset Strict Implicit.
+
+CoInductive LList (A : Set) : Set :=
+  | LNil : LList A
+  | LCons : A -> LList A -> LList A.
+
+Implicit Arguments LNil [A].
+
+Inductive Finite (A : Set) : LList A -> Prop :=
+  | Finite_LNil : Finite LNil
+  | Finite_LCons :
+      forall (a : A) (l : LList A), Finite l -> Finite (LCons a l).
+
+(* Check positivity modulo reduction (cf bug #983) *)
 
-CoInductive LList [A:Set] : Set :=
-   | LNil : (LList A)
-   | LCons : A -> (LList A) -> (LList A).
+Record P:Type := {PA:Set; PB:Set}.
 
-Implicits LNil [1].
+Definition F (p:P) := (PA p) -> (PB p).
 
-Inductive Finite [A:Set] : (LList A) -> Prop :=
-   | Finite_LNil : (Finite LNil)
-   | Finite_LCons : (a:A) (l:(LList A)) (Finite l) -> (Finite (LCons a l)).
+Inductive I_F:Set := c : (F (Build_P nat I_F)) -> I_F.