The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

There are times when certain case analysis tactics can be used to 
replace the hypothesis they are used on.  For instance, something like 
"induction H as [H ...]."  This is convenient.  However, I just noticed 
that it matters as to whether H is a local hypothesis in the definition, 
or if it is a section variable.  As a section variable, this replacing 
via intro pattern does not work - but it does still work to do this the 
long way as "induction H as [H' ...]. clear H. rename H' into H."

Is this a bug or a feature?  I only noticed it because it broke one of 
my tactics - but I can of course just use the clear/rename workaround.  
I am just curious why there might be any difference at all between the 
two case.

-- Jonathan