Skip to content

Commit 77ef757

Browse files
committed
Rocq warnings: address the new warning names introduced by Rocq Stdlib 9.2
`-deprecated-XXX-since-YY.ZZ` is now `-deprecated-XXX-since-Stdlib-YY.ZZ`. Old warning names are still mentioned, for compatibility with Stdlib <= 9.1.
1 parent 5074ecc commit 77ef757

1 file changed

Lines changed: 8 additions & 1 deletion

File tree

‎Makefile‎

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,9 @@ endif
5454
# deprecated-since-8.19
5555
# deprecated-since-8.20
5656
# deprecated-reference-since-9.0
57+
# deprecated-reference-since-Stdlib-9.0
5758
# deprecated-reference-since-9.1
59+
# deprecated-reference-since-Stdlib-9.1
5860
# renamings performed in Coq's standard library;
5961
# using the new names would break compatibility with earlier Coq versions.
6062
# deprecated-from-Coq
@@ -74,7 +76,9 @@ COQCOPTS ?= \
7476
-w -deprecated-since-8.19 \
7577
-w -deprecated-since-8.20 \
7678
-w -deprecated-reference-since-9.0 \
79+
-w -deprecated-reference-since-Stdlib-9.0 \
7780
-w -deprecated-reference-since-9.1 \
81+
-w -deprecated-reference-since-Stdlib-9.1 \
7882
-w -deprecated-from-Coq \
7983
-w -register-all \
8084
-w -notation-for-abbreviation \
@@ -96,8 +100,11 @@ cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality -w -depr
96100
flocq/%.vo MenhirLib/%.vo: COQCOPTS+=\
97101
-w -deprecated-syntactic-definition \
98102
-w -deprecated-since-9.0 \
103+
-w -deprecated-since-Stdlib-9.0 \
99104
-w -deprecated-since-9.1 \
100-
-w -deprecated-since-9.2
105+
-w -deprecated-since-Stdlib-9.1 \
106+
-w -deprecated-since-9.2 \
107+
-w -deprecated-since-Stdlib-9.2
101108

102109
# For the extraction phase, we silence other warnings:
103110
# change-dir-deprecated:

0 commit comments

Comments
 (0)