Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • S stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 79
    • Issues 79
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 14
    • Merge requests 14
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • stdpp
  • Merge requests
  • !17

Use `stdpp_scope` for all notations.

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Robbert Krebbers requested to merge stdpp_scope into master Nov 09, 2017
  • Overview 10
  • Commits 1
  • Pipelines 0
  • Changes 5

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 Nov 09, 2017 by Robbert Krebbers
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: stdpp_scope