1 files changed, 56 insertions, 43 deletions
diff --git a/test-suite/success/Case12.v b/test-suite/success/Case12.v
index 284695f4..f6a0d578 100644
--- a/test-suite/success/Case12.v
+++ b/test-suite/success/Case12.v
@@ -1,60 +1,73 @@
 (* This example was proposed by Cuihtlauac ALVARADO *)
 
-Require PolyList.
+Require Import List.
 
-Fixpoint mult2 [n:nat] : nat :=
-Cases n of
-| O => O
-| (S n) => (S (S (mult2 n)))
-end.
+Fixpoint mult2 (n : nat) : nat :=
+  match n with
+  | O => 0
+  | S n => S (S (mult2 n))
+  end.
 
 Inductive list : nat -> Set :=
-| nil : (list O)
-| cons : (n:nat)(list (mult2 n))->(list (S (S (mult2 n)))).
+  | nil : list 0
+  | cons : forall n : nat, list (mult2 n) -> list (S (S (mult2 n))).
 
 Type
-[P:((n:nat)(list n)->Prop);
- f:(P O nil);
- f0:((n:nat; l:(list (mult2 n)))
-      (P (mult2 n) l)->(P (S (S (mult2 n))) (cons n l)))]
- Fix F
-   {F [n:nat; l:(list n)] : (P n l) :=
-      <P>Cases l of
-        nil => f
-      | (cons n0 l0) => (f0 n0 l0 (F (mult2 n0) l0))
-      end}.
+  (fun (P : forall n : nat, list n -> Prop) (f : P 0 nil)
+     (f0 : forall (n : nat) (l : list (mult2 n)),
+           P (mult2 n) l -> P (S (S (mult2 n))) (cons n l)) =>
+   fix F (n : nat) (l : list n) {struct l} : P n l :=
+     match l as x0 in (list x) return (P x x0) with
+     | nil => f
+     | cons n0 l0 => f0 n0 l0 (F (mult2 n0) l0)
+     end).
 
 Inductive list' : nat -> Set :=
-| nil' : (list' O)
-| cons' : (n:nat)[m:=(mult2 n)](list' m)->(list' (S (S m))).
+  | nil' : list' 0
+  | cons' : forall n : nat, let m := mult2 n in list' m -> list' (S (S m)).
 
-Fixpoint length [n; l:(list' n)] : nat :=
-  Cases l of
-     nil' => O
-  | (cons' _ m l0) => (S (length m l0))
+Fixpoint length n (l : list' n) {struct l} : nat :=
+  match l with
+  | nil' => 0
+  | cons' _ m l0 => S (length m l0)
   end.
 
 Type
-[P:((n:nat)(list' n)->Prop);
- f:(P O nil');
- f0:((n:nat)
-      [m:=(mult2 n)](l:(list' m))(P m l)->(P (S (S m)) (cons' n l)))]
- Fix F
-   {F [n:nat; l:(list' n)] : (P n l) :=
-      <P>
-        Cases l of
-          nil' => f
-        | (cons' n0 m l0) => (f0 n0 l0 (F m l0))
-        end}.
+  (fun (P : forall n : nat, list' n -> Prop) (f : P 0 nil')
+     (f0 : forall n : nat,
+           let m := mult2 n in
+           forall l : list' m, P m l -> P (S (S m)) (cons' n l)) =>
+   fix F (n : nat) (l : list' n) {struct l} : P n l :=
+     match l as x0 in (list' x) return (P x x0) with
+     | nil' => f
+     | cons' n0 m l0 => f0 n0 l0 (F m l0)
+     end).
 
 (* Check on-the-fly insertion of let-in patterns for compatibility *)
 
 Inductive list'' : nat -> Set :=
-| nil'' : (list'' O)
-| cons'' : (n:nat)[m:=(mult2 n)](list'' m)->[p:=(S (S m))](list'' p).
-
-Check Fix length { length [n; l:(list'' n)] : nat :=
-         Cases l of
-           nil'' => O
-         | (cons'' n l0) => (S (length (mult2 n) l0))
-         end }.
+  | nil'' : list'' 0
+  | cons'' :
+      forall n : nat,
+      let m := mult2 n in list'' m -> let p := S (S m) in list'' p.
+
+Check
+  (fix length n (l : list'' n) {struct l} : nat :=
+     match l with
+     | nil'' => 0
+     | cons'' n l0 => S (length (mult2 n) l0)
+     end).
+
+(* Check let-in in both parameters and in constructors *)
+
+Inductive list''' (A:Set) (B:=(A*A)%type) (a:A) : B -> Set :=
+  | nil''' : list''' A a (a,a)
+  | cons''' : 
+     forall a' : A, let m := (a',a) in list''' A a m -> list''' A a (a,a).
+
+Fixpoint length''' (A:Set) (B:=(A*A)%type) (a:A) (m:B) (l:list''' A a m) 
+  {struct l} : nat :=
+  match l with
+  | nil''' => 0
+  | cons''' _ m l0 => S (length''' A a m l0)
+  end.