The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 24/02/2015 07:20, Sriram Srinivasan wrote:
> Can someone explain why the following doesn't work in 8.5beta1?
>
> 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.

Constructors and destructors are no longer separate in 8.5. Since the 
constructor nil takes an argument, the destructor nil also takes an 
argument. Since this argument is noninformative, it has to be "_".

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

You can recover the old behavior by using

Set Asymmetric Patterns.

Best regards,

Guillaume