Skip to content
Snippets Groups Projects

compatibility with rocq (aka Coq) 9.0

Closed Johannes Hostert requested to merge rocq-9.0 into master
1 unresolved thread
2 files
+ 4
1
Compare changes
  • Side-by-side
  • Inline
Files
2
+ 3
0
@@ -6,6 +6,9 @@
-arg -w -arg -redundant-canonical-projection
# Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
-arg -w -arg -notation-incompatible-prefix
# We can't do this migration yet until we require Coq 9.0
-arg -w -arg -deprecated-from-Coq
-arg -w -arg -deprecated-dirpath-Coq
    • Comment on lines +9 to +11

      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
theories/logic/satisfiable.v
theories/simulation/language.v
Loading