Skip to content

GitLab

  • Menu
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 153
    • Issues 153
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 8
    • Merge requests 8
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • 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
Reviewer
Request review from
Time tracking
Source branch: ralf/drop-8.12