The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

You can also use:

Set Implicit Arguments.

and remove the argument X:

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

Le 24/02/2015 07:31, Guillaume Melquiond a écrit :
> 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