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 81
    • Issues 81
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 12
    • Merge requests 12
  • 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
  • !156

Alternative take on #153: fix `le` in future versions of Coq

  • Review changes

  • Download
  • Email patches
  • Plain diff
Closed Robbert Krebbers requested to merge ci/robbert/arith into master May 05, 2020
  • Overview 27
  • Commits 3
  • Pipelines 2
  • Changes 4

This should provide compatibility for https://github.com/coq/coq/pull/12162

Other changes:

  • Use Arith instead of NPeano, since the latter is deprecated. While it may also be possible to import NPeano, numbers export PArith NArith ZArith, so it seemed logical to also export Arith.
  • Add test to check for correct version of le.
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: ci/robbert/arith