Skip to content
Snippets Groups Projects
Commit 21aaa5d3 authored by Ralf Jung's avatar Ralf Jung
Browse files

silence Coq 8.20 deprecation warnings

parent 5da2f2e2
No related branches found
No related tags found
No related merge requests found
Pipeline #106960 failed
Stage: build
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 0 deletions
_CoqProject
+ 2
− 0
View file @ 21aaa5d3
...@@ -7,6 +7,8 @@ ...@@ -7,6 +7,8 @@
# Custom flags (to be kept in sync with the dune file at the root of the repo). # Custom flags (to be kept in sync with the dune file at the root of the repo).
# Fixing this one requires Coq 8.19 # Fixing this one requires Coq 8.19
-arg -w -arg -argument-scope-delimiter -arg -w -arg -argument-scope-delimiter
# Fixing this requires Coq 8.20.
-arg -w -arg -deprecated-since-8.20
stdpp/options.v stdpp/options.v
stdpp/base.v stdpp/base.v
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment