The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

On 03/08/14 13:06, Gabriel Scherer wrote:
> One man's random garbage is another's perfectly valid variable name.
> Matej was, however, getting an error message, highlighting the extra
> cases after the free variable.
> 
>> Error: this clause is redundant.
> 
> It's delicate to design languages with pattern-matching that never
> behave confusingly. In OCaml, variables may not start with an
> uppercase, precisely to avoid this problem. In some other languages,
> variables are not patterns by themselves, you have to use some
> explicit marker to turn a variable in a binder pattern. That's also
> rather heavy.

My caution against typos in variable names was dulled by Ocaml.

There, instead of:

        Toplevel input, characters ...-...:
        >     | April | June | September | November => true
        >       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
        Error: this clause is redundant.

I would get:

        Toplevel input, characters ...-...:
              | Feburary => negb leap
                ^^^^^^^^
        Warning: Unused variable "Feburary"

        Toplevel input, characters ...-...:
        >     | April | June | September | November => true
        >       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
        Error: This clause is redundant.

which, however simple it sounds, would lead me to the right direction.

Until unused variables are detected by Coq automatically, I just have to be 
more careful.

Thank you guys.