The Coq mailing list

[Stefan Holdermans <stefan AT cs.uu.nl>]

Adam,

Thank you for your quick answer.

> This is one of the most common problems in getting started with Coq.  
> [induction] only works over predicates applied to arguments that are  
> all variables. In your case, one of the arguments is [S n]. I would  
> prefer that Coq signal an error in this case. Instead, the current  
> [induction] implementation replaces each complex term with a fresh  
> variable, forgetting structural details.

That is indeed a severe restriction. The workaround you describe is  
the one I had taken, but it felt quite clumsy. Still, I can live with  
it. :-)

Cheers,

  Stefan