The option is documented but is missing an index. See https://coq.inria.fr/distrib/current/refman/gallina-ext.html#hevea_command71. I don't know what Print Tables so I can't comment on this.

FTR, it's not displayed by Print Tables because it is not an option but a command. It would be nice if it were an option, but we can't do it that because it can take a list of variables as arguments.

Is there any way to dump all the "option-like" state in Coq? The fact that this is not printed meant it took me really long to even figure out why the same code behaves different in one file vs. another.

@Zimmi48

The option is documented but is missing an index. See https://coq.inria.fr/distrib/current/refman/gallina-ext.html#hevea_command71.

That documentation is incomplete then, it fails to mention the effect on Instance.

Should I open a separate bug asking for a way to have generalization in `{...} but not in Instance?

Given how weird the effect on Instance is, and that this effect is not documented, I would consider it a bug (even if I'm pretty sure that @mattam82 intended for this behavior). Yes, please open a request for an option to decide if Generalize All Variables has a special effect on Instance.

I moved separating the two effects to a new issue #6888. This is now just about the lack of documentation.

Note that this isn't specific to generalizable all variables (see this example) - it's just that implicit generalization in instances does not require any syntax, which is indeed surprising and I agree that it should at least be possible to disable the instance generalization, even if that remains the default.

I'm taking the liberty of closing this issue because it seems fixed. Feel free to reopen this, or open a new issue with an up-to-date description of what should happen now.

Rationale:

• The issue on the actual behavior is Provide Generalizable All Variables without an effect on Instance #6042 (now fixed). So there's no need to document the effect on Instance — which seems the point of this issue.
• There are docs at https://coq.inria.fr/distrib/current/refman/language/extensions/implicit-arguments.html#implicit-generalization; they document everything I'm aware of.
• Finally, the command index points to https://coq.inria.fr/distrib/current/refman/language/extensions/implicit-arguments.html#coq:cmd.Generalizable which seems accurate.