Stop relying on auto-generated names in stdlib (re: name mangling)

Proofs in the stdlib currently rely on auto-generated names in lots of places (one example I was looking at today while attempting coq/coq#6607, here the H on the second line is not introduced, but this is a really pervasive phenomenon). As suggested in coq/coq#2301, I believe that this makes proofs harder to maintain, and makes it more difficult to change other parts of the system.

I have specifically run into issues with the current state when trying coq/coq#6607 and when trying to simplify the intuition tactic.

Working on top of coq/coq#6582, I would like to edit the proofs in the standard library so that it compiles with the -mangle-names "_" option.

I see this providing several benefits:

• A stdlib more robust to changes in the rest of Coq
• Experience writing proofs in this style, which may provide motivation to make the process easier
• Assuming we also consider the robust style good practice, leading by example

A possible problem with this is that the test suite becomes less sensitive to changes in generated names, making it easier for changes to break users not writing robust proofs (especially unnoticed by developers).

As long as the changes are confined to Opaque proofs, or in the case of transparent terms built with tactics limited to providing explicit names, I don't see any potential for compatibility issues.

This process should produce incremental benefits, so even if I run out of steam partway through there is no wasted work.

I have heard rumors of work on a stdlib2 by @maximedenes in the future. However, I do not believe there are plans for the current stdlib to disappear in say the next year given how much work is dependent on it. Therefore I hope this has benefit independent of stdlib2.

I am volunteering to edit the proofs (in what free time I have), but I would need someone to review the pull requests I generate. Is there someone who is willing and able to do this? (@herbelin? @ppedrot? Who is responsible for maintaining the standard library?)