Use -deprecated-since-N.NN warning options

For finer control of deprecation warnings.

Author: xavierleroy

Makefile

@@ -57,13 +57,25 @@ endif
 # deprecated-instance-without-locality:
 #    warning introduced in 8.14
 #    triggered by Menhir-generated files, to be solved upstream in Menhir
+# deprecated-since-8.19
+# deprecated-since-8.20
+#    renamings performed in Coq's standard library;
+#    using the new names would break compatibility with earlier Coq versions.
 
 COQCOPTS ?= \
-  -w -unused-pattern-matching-variable
+  -w -unused-pattern-matching-variable \
+  -w -deprecated-since-8.19 \
+  -w -deprecated-since-8.20
 
 cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality
 MenhirLib/Interpreter.vo: COQCOPTS += -w -undeclared-scope
 
+# Flocq and Menhirlib run into other renaming issues.
+# These warnings can only be addressed upstream.
+
+flocq/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition
+MenhirLib/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition
+
 ifneq ($(INSTALL_COQDEV),true)
 # Disable costly generation of .cmx files, which are not used locally
   COQCOPTS += -w -deprecated-native-compiler-option -native-compiler no
@@ -219,12 +231,6 @@ endif
 
 proof: $(FILES:.v=.vo)
 
-# Turn off some warnings for Flocq and Menhirlib
-# These warnings can only be addressed upstream
-
-flocq/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition
-MenhirLib/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition
-
 extraction: extraction/STAMP
 
 extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v $(ARCH)/extractionMachdep.v