Use `stdpp_scope` for all notations.

A long time ago, stdpp was part of my C formalization, and as such, I used C_scope for all notations in the development. These days, the name of this scope totally makes no sense, and even confuses new users of the library, especially now that the project has a project name (coq-stdpp)

I thus propose to rename C_scope into stdpp_scope and the scope delimiter %C into %stdpp. It should be very trivial to fix this in all dependencies; we should just provide a sed script.

changed the description

I am not very happy with %stdpp being so long.

I don't see the problem. In Iris, for example, we have 8 occurrences of %C, out of which 7 appear in notations.

And 0 in lambdaRust.

iGPS has at least 30.

What's the reason there are so many? @janno?

I managed to get rid of all %C scopes in iGPS, I will submit an MR to iGPS soon.

https://gitlab.mpi-sws.org/FP/sra-gps/merge_requests/14

Well, I guess that defeats my argument. LGTM!

Alright, @janno can you let me know whether you are ok with this (and the iGPS MR), then I will merge this.

Janno merged https://gitlab.mpi-sws.org/FP/sra-gps/merge_requests/14, so I will merge this :).

mentioned in commit 30f481c2

merged