The Coq mailing list

[Vilhelm Sj�berg <vilhelm AT cis.upenn.edu>]

On Thu, Nov 03, 2011 at 03:12:32PM -0400, Andrew Pennebaker wrote:
> Definition one : nat := S O.
> Definition two : nat := S(S O).
> 
> Fixpoint fib (n : nat) : nat :=
> match n with
> | O => O
> | one => one
> | _ => plus (fib (minus n one)) (fib (minus n two))
> end.
> 
> When I tell CoqIDE to go forward with the fib function, it reports "Error:
> This clause is redundant", and underlines the last case in fib:
> 
> _ => plus (fib (minus n one)) (fib (minus n two))
> 
> What am I doing wrong?

"one" gets interpreted as a variable bound by the match. You need to write 
out 
the term using constructors:
 | (S O) => one

Vilhelm Sjoberg