Should auto-generated schemes be moved inside there own modules/records about stdlib2 HOT 2 OPEN

These are two different issues though.

1. Uniform naming or namespacing of schemes
2. Allowing to (re)bind schemes to arbitrary definitions.

The second point is fairly easy to implement, but depending on the reading, the first one might be impossible in the current CIC theory.

from stdlib2.

we cannot change the default induction principle

We can prevent the generation of induction principles and then define our own. How would the module / record approach affect this?

We cannot easily blacklist induction principles from Search... Yes we can but with the "_ind" which may blacklist other lemmas.

How would that change?

Anyway, I am supportive of this proposal but I'm afraid something is missing from Coq (namespaces) to do it properly. Indeed, the issue with modules or records is that you cannot reopen them. What would be useful is namespaces that you can reopen.

EDIT: posted independently of @ppedrot's comment just above.

from stdlib2.