The notation Structure.on and Structure.Build should be better scoped

[CohenCyril]

Indeed, writing Equality.on (nat * nat) will mistakenly interpret * as being the natural number multiplication instead of the cartesian product. The same goes for Build.

We should use the scope given by the type of the argument, and allow manual overriding from the user.

Spotted by @ggonthier

[gares]

In Coq we have the APIs now.
But I did not expose it to coq-elpi:
https://github.com/LPCIC/coq-elpi/blob/069018b9009f9bc5179cb08d714d681a114d6e14/src/coq_elpi_builtins.ml#L3114-L3130

[gares]

The only design choice to make is how to pass the info to

coq.notation.add-abbreviation "foo" 3 {{ fun x y z => term }} OnlyParsing Abbrev

since the types of x y z are currently ignored, we could use them, but how to encode a scope name there is unclear.
maybe a scope : string -> Type constant and write

{{ fun x : scope "type_scope" => ... }}