Skip to content
Snippets Groups Projects

compatibility with rocq (aka Coq) 9.0

compatibility with rocq (aka Coq) 9.0
rocq-9.0 into master
1 unresolved thread
Closed Johannes Hostert requested to merge rocq-9.0 into master
1 unresolved thread

basically everything still works. cc @jung

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
_CoqProject
6 6 -arg -w -arg -redundant-canonical-projection
7 7 # Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
8 8 -arg -w -arg -notation-incompatible-prefix
9 # We can't do this migration yet until we require Coq 9.0
10 -arg -w -arg -deprecated-from-Coq
11 -arg -w -arg -deprecated-dirpath-Coq
  • Comment on lines +9 to +11
    Ralf Jung
    Ralf Jung @jung ·
    Owner

    These would still be good to have in preparation for when we add 9.0 to CI. Do they fix all the warnings or are there more?

  • Please register or sign in to reply
Please register or sign in to reply