Tweak warning options for Coq/Rocq 9.0

Author: xavierleroy

Makefile

@@ -61,29 +61,35 @@ endif
 # deprecated-since-8.20
 #    renamings performed in Coq's standard library;
 #    using the new names would break compatibility with earlier Coq versions.
+# deprecated-from-Coq
+#    Rocq wants "From Stdlib Require" while Coq wants "From Coq Require".
 
 COQCOPTS ?= \
   -w -unused-pattern-matching-variable \
   -w -deprecated-since-8.19 \
-  -w -deprecated-since-8.20
+  -w -deprecated-since-8.20 \
+  -w -deprecated-from-Coq
 
 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
+flocq/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition -w -deprecated-since-9.0
+MenhirLib/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition -w -deprecated-since-9.0
 
 # For the extraction phase, we silence other warnings:
 # change-dir-deprecated:
 #    warning introduced in 8.20, no alternative before 8.20
 # extraction-default-directory:
 #    warning introduced in 8.20, no alternative before 8.20
+# deprecated-from-Coq:
+#    see above
 COQEXTRACTOPTS ?= \
   -w -change-dir-deprecated \
-  -w -extraction-default-directory
+  -w -extraction-default-directory \
+  -w -deprecated-from-Coq
 
 ifneq ($(INSTALL_COQDEV),true)
 # Disable costly generation of .cmx files, which are not used locally