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 10
    • Merge requests 10
  • 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
  • !437

Enable `Hint Mode Equiv` now that stdpp requires Coq 8.12

  • Review changes

  • Download
  • Email patches
  • Plain diff
Open Paolo G. Giarrusso requested to merge Blaisorblade/stdpp:mode-equiv into master Dec 16, 2022
  • Overview 5
  • Commits 2
  • Pipelines 2
  • Changes 5

Includes fixes for Coq 8.12/8.13 — but we might want to drop those.

Rationale: while Coq bug https://github.com/coq/coq/issues/14441 is still relevant, Iris chose to pay the costs of those annotations. Back then, stdpp didn't because it still supported Coq 8.11 which suffered from additional bugs (fixed in 8.12) — Iris still has this comment:

 (* No Hint Mode set in stdpp because of Coq bugs #5735 and #9058, only
 fixed in Coq >= 8.12, which Iris depends on. *)
Edited Dec 17, 2022 by Paolo G. Giarrusso
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: mode-equiv