You should probably turn this option off in the compatibility file Coq87.v.

You should probably turn this option off in the compatibility file Coq87.v.

No, the default behaviour is the 8.7 behaviour.

Thanks!

IIRC 8.7 does not generalize typeclass instance variables per default, but only if Generalizable All Variables is set.

Also, what is the interaction of the new option with Generalizable All Variables?

It only generalizes those variables which are generalizable.
Basically we have preexisting syntax Instance foo : !bar which disables generalization, new syntax

Instance foo : `bar

which enables it and without an explicit marker the option decides which is picked (with 8.7 always picking `)

Github using ` for code blocks is a pain.

But that changes behavior, right? The following currently passes:

Class Bar (n:nat) := {}.
Fail Instance bar : Bar n := {}.

With your PR, because it defaults to `, this will fail, no?

It already defaults to `. This PR only adds an option to switch the default and explicit syntax to pick `.

Ah, so ` actually just has no effect unless Generalizable All Variables is set?

It's probably more complicated than that. ` avoids running some implicit_application transformation on the type of the instance, but I don't quite understand what's going on.
Could use some help.

Like what is going on here 95dd730

If I come back to this issue I probably won't base my work on this PR.

I opened an issue at #6888 to make sure this doesn't get forgotten.