I recently learned that in Coq, we can mark a definition as not being imported with Import/Export. I think we should explore the option of using this to mark definitions that are internal to a module and should not be used by clients -- those then don't need the C-style namespacing of prefixing everything.

As a random example for such definitions, consider these.