Skip to content

Commit b700143

Browse files
committed
Disable new warnings in Rocq 9
1 parent dbd5c60 commit b700143

File tree

1 file changed

+1
-3
lines changed

1 file changed

+1
-3
lines changed

_CoqProject

+1-3
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,7 @@
88
-arg -w -arg +deprecated-tactic-notation
99
-arg -w -arg -deprecated-since-8.19
1010
-arg -w -arg -deprecated-since-8.20
11-
# std lib moved from Coq to Stdlib; will be available in Coq 8.21
12-
-arg -w -arg -deprecated-from-Coq
13-
-arg -w -arg -deprecated-dirpath-Coq
11+
-arg -w -arg -deprecated-since-9.0
1412
# seems to have false positives
1513
-arg -w -arg -notation-incompatible-prefix
1614
# we haven't updated our code to fix this one

0 commit comments

Comments
 (0)