Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Register
  • Sign in
  • S stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 84
    • Issues 84
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 9
    • Merge requests 9
  • 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
  • !445

Add locality for `Hint Rewrite`.

  • Review changes

  • Download
  • Patches
  • Plain diff
Merged Robbert Krebbers requested to merge robbert/hint_rewrite_locality into master Feb 13, 2023
  • Overview 5
  • Commits 2
  • Pipelines 2
  • Changes 5

We can do this since we dropped support for Coq 8.13.

For natmap, the apply to internal lemmas and should thus be Local.

For the bit files, it appears the rewrites are used in a tactic that is used externally. Hence they should be Global.

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: robbert/hint_rewrite_locality