Skip to content
Snippets Groups Projects
Commit f4332e32 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Add support for Coq version 8.17.0.

parent 03eaffa3
No related branches found
No related tags found
No related merge requests found
......@@ -17,6 +17,9 @@
-arg -w -arg -redundant-canonical-projection
# Fixing this one requires Coq 8.15.
-arg -w -arg -deprecated-typeclasses-transparency-without-locality
# Disabling warnings about future coercion syntax that requires Coq 8.17
# (https://github.com/coq/coq/pull/16230)
-arg -w -arg -future-coercion-class-field
iris/prelude/options.v
iris/prelude/prelude.v
......
......@@ -27,7 +27,7 @@ tags: [
]
depends: [
"coq" { (>= "8.13" & < "8.17~") | (= "dev") }
"coq" { (>= "8.13" & < "8.18~") | (= "dev") }
"coq-stdpp" { (= "dev.2023-03-24.1.504d165a") | (= "dev") }
]
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment