The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

I already reported a probably related bug in 2010:

https://coq.inria.fr/bugs/show_bug.cgi?id=2243

It was about destruct and not clear.

2014-06-25 8:27 GMT+02:00 Guillaume Melquiond <guillaume.melquiond AT inria.fr>:

On 24/06/2014 19:56, Jonathan wrote:

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.

The discrepancy between induction and clear is indeed a bug. Whether the bug is in induction or clear is not that obvious though. Not so long ago (I haven't tested if it is still true), it was possible to write ill-formed proofs by clearing section variables. Fortunately, Coq would catch the issue at Qed, but still this was hardly satisfactory. Worse, clearing section variables would also cause Coq to reject some well-formed proofs.

Best regards,

Guillaume

--
.../Sedrikov\...