The Coq mailing list

[Rene Vestergaard <vester AT jaist.ac.jp>]

When inputting "Print nat_rect." to the current Windows version (8.0, 
April 2004), I get the following response:

nat_rect =
fun (P : nat -> Type) (f : P 0) (f0 : forall n : nat, P n -> P (S n)) =>
(fix F (n : nat) : P n :=
   match n return P with
   | O => f
   | S n0 => f0 n0 (F n0)
   end)
     : forall P : nat -> Type,
       P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

Should it not be "match n return (P n)"?

Cheers,
/R