Fix style: split asymmetric patterns commands onto separate lines

[Copilot]

• Split Set Asymmetric Patterns. and #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. onto separate lines in all 127 affected files
• Put the #[warning="-unknown-option"] attribute on its own line (separate from the command it applies to)
• Add comment in theories/Basics/Settings.v noting the warning clause can be removed once minimum Rocq version is 9.3

[jdchristensen]

This is an improvement, but I'd actually prefer a line break after the warning clause as well.
Also, near this line in theories/Basics/Settings.v, it would be good to add a comment like:
"The warning clause here and in other parts of the library can be removed once our minimum Rocq version is 9.3."

[Alizter]

This is an improvement, but I'd actually prefer a line break after the warning clause as well. Also, near this line in theories/Basics/Settings.v, it would be good to add a comment like: "The warning clause here and in other parts of the library can be removed once our minimum Rocq version is 9.3."

@copilot do this please.

To be clear the suggestion is:

Vernac_command_one.
(* Explanation about version *)
#[warning....]
Vernac_command_two.

Only the one in settings.v needs the explanation the others just need their style adjusted.

[Copilot]

This is an improvement, but I'd actually prefer a line break after the warning clause as well.
Also, near this line in theories/Basics/Settings.v, it would be good to add a comment like:
"The warn...

Done in fa220fc. The #[warning="-unknown-option"] attribute is now on its own line (separate from the command it applies to) across all 127 files, and theories/Basics/Settings.v has the comment noting when the warning clause can be removed.

[jdchristensen]

@copilot Can you squash the two commits into one?

[Copilot]

@copilot Can you squash the two commits into one?

Squashing requires a force push which I'm unable to do with the tools available to me. You could either squash the commits locally and force push, or use GitHub's "Squash and merge" option when merging the PR to land it as a single commit.

[jdchristensen]

Copilot couldn't squash it, and we don't seem to have that option with the merge button, so I'm fine with it being merged as is.

@copilot The first comment in the PR says that it has been squashed, so that should be removed since the squash failed.

[jdchristensen]

@copilot The first comment in the PR says that it has been squashed, so that should be removed since the squash failed.

[Copilot]

@copilot The first comment in the PR says that it has been squashed, so that should be removed since the squash failed.

Removed the "squashed" line from the PR description.

[Alizter]

Unfortunately Copilot is not good at rewriting its git history. I'll check this PR out later locally and fix it up.