Skip to content

Use `stdpp_scope` for all notations.

Robbert Krebbers requested to merge stdpp_scope into master

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

Merge request reports