setoid rewriting: improve support for forall_relation

[MathisBD]

This PR improves the support for forall_relation in setoid rewriting:

1. Added support for forall_relation in the normalization wrt flip algorithm of setoid rewriting.
2. Added a notation for forall_relation in scope signature_scope which allows writing instances like Proper (R ==> ∀ x y, S) with x and y appearing in S.

[MathisBD]

There seems to be lots of trailing whitespace removed in the diff, someone knows what's going on?

[MathisBD]

Ah it seems that Notation "∀ x .. y , R" := ... will not work because it's already used elsewhere. What do you suggest? Not exporting the notation by default, so that users have to do something like Import ProperForallNotation, or using a different notation?

[Lysxia]

There seems to be lots of trailing whitespace removed in the diff, someone knows what's going on?

Probably your editor (or git) is configured to auto-delete trailing whitespace and you probably want to disable it.

Ah it seems that Notation "∀ x .. y , R" := ... will not work because it's already used elsewhere.

How about forallR?

[MathisBD]

Probably your editor (or git) is configured to auto-delete trailing whitespace and you probably want to disable it.

Yes my editor is doing this. I'm confused now: doesn't Rocq have a policy of no trailing whitespace in source files?

How about forallR?

Why not. What do others think?

[thomas-lamiaux]

The linter is supposed to reject trailing white spaces, I don't know what is up. @SkySkimmer ?

(It might be that the modif are checked not to introduce trailing white spaces but not that the whole project is without 🤷)

[thomas-lamiaux]

Suggested change

	Qed.
	Qed.

[SkySkimmer]

We check that changed lines don't have trailing whitespace but we allow old trailing whitespace to exist

[mattam82]

Probably your editor (or git) is configured to auto-delete trailing whitespace and you probably want to disable it.

Yes my editor is doing this. I'm confused now: doesn't Rocq have a policy of no trailing whitespace in source files?

It does now, but on existing files we avoid brutally doing it for easier diff reading and blaming.

How about forallR?

Why not. What do others think?

Fine with me