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.
Edited by Robbert Krebbers