Proof using should clear the context

[nomeata]

I started using Proof using to get parallel processing of proofs in sections. But I think the feature could be even more useful if it also clears the context of any section variables that, according to the Proof using specification, may not be used.

[SkySkimmer]

There's the option Proof Using Clear Unused to do that.
See discussion at #883 about making it default on.

[nomeata]

Ah nice!

Is that already in 8.8? If so, then this issue is about https://coq.inria.fr/refman/proof-engine/proof-handling.html not mentioning it :-)

[gares]

I'm not sure we should document the option. While it would be the natural thing to do, clearing section variables breaks things in very bad ways. One day this option will be on, I hope. I recommend to read #883 before turning this option on.

[gares]

Duplicate of #883

[maximedenes]

I'm not sure we should document the option. While it would be the natural thing to do, clearing section variables breaks things in very bad ways.

I think this is an argument strongly in favor of documenting it, and explaining why it is dangerous, instead.

[gares]

CC @CohenCyril that asked me this very question 5 seconds ago

[gares]

I find it silly to put a self-destruction button on your car, but even sillier to make it easy to find and document that you should not use it.

Don't think about the pink elephant!

I'm half guilty for the first silliness (I was ignorant of the effects at the time). I won't be guilty for the latter.

[SkySkimmer]

see also #22113