The Coq mailing list

[Sriram Srinivasan <sriram AT malhar.net>]

Can someone explain why the following doesn't work in 8.5beta1? 

Thanks much.


Inductive list (X:Type) : Type :=
  | nil : list X
  | cons : X -> list X -> list X.


Fixpoint length (X:Type) (l:list X) : nat :=
  match l with
  |nil  => 0
  |cons h t => S (length X t)
  end.

Error:  The constructor nil (in type list) expects 1 argument.