The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 06/25/2014 03:46 AM, Cedric Auger wrote:
> 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.

That is even stranger, as it won't allow the section variable to be 
destructed prior to renaming it.  Or, rather, that the original name is 
tied to some unseen dependency.  For instance, I tried this with your 
test case: revert H; intro L; revert L; intro H; destruct H. - and it 
still fails the same way: "Error: H is used in hypothesis i."  Even this 
sequence fails in your setup:

  revert H.
  assert (H:True) by constructor.
  destruct H; clear H. (* shows H:True can be destructed *)
  intro H.
  destruct H. (*fails*)

Also, if one removes the "Section 0" line, forcing the variables to 
become local definitions, then the destruct works.


In the case I reported, I was able to destruct the variable as long as I 
did so by only introducing new ids.  I was able to verify that my case 
occurs with destruct as well as induction.

I guess I should restrict usage of section variables until this is fixed...

-- Jonathan