Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 171
    • Issues 171
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 15
    • Merge requests 15
  • 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
  • IrisIris
  • Merge requests
  • !763

drop support for Coq 8.12

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Ralf Jung requested to merge ralf/drop-8.12 into master Dec 04, 2021
  • Overview 3
  • Commits 1
  • Pipelines 2
  • Changes 3

I am proposing we drop support for Coq 8.12. This is in line with the usual policy of supporting the latest 2 stable releases. Coq 8.13 has been out for half a year, giving a lot of time to port developments.

Requiring Coq 8.13 will let us finally use v closed binder in notation such as big-ops or WP, enabling type annotations. It also lets us land !762 (merged).

Edited Dec 04, 2021 by Ralf Jung
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: ralf/drop-8.12