Should auto-generated schemes be moved inside there own modules/records

[Matafou]

Opening a discusison:

I am not sure this is in the scope of stdlib2 or if this is already thought of, but it would be nice to move all default auto-generated schemes (foo_ind... beq_foo etc) into there own modules (or record) and have a command to change the default "default scheme module". For instance the current "_ind" name trick is painful at least for the 2 following reasons

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

[ppedrot]

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.

[Zimmi48]

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.