Skip to content
Snippets Groups Projects

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

Closed Robbert Krebbers requested to merge ci/robbert/arith into master

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.

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
Please register or sign in to reply
Loading