Skip to content

Commit 9dfe9be

Browse files
committed
Do not warn for deprecations in 8.20, 9.0
1 parent 42016df commit 9dfe9be

File tree

1 file changed

+1
-2
lines changed

1 file changed

+1
-2
lines changed

Makefile

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -519,8 +519,7 @@ print_DEPFLAGS:
519519
SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g'
520520
EXISTING_COQPROJECT_CONTENTS_SORTED:=$(shell cat _CoqProject 2>&1 | $(SORT_COQPROJECT))
521521
WARNINGS_PLUS := +implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+undeclared-scope,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+deprecated-typeclasses-transparency-without-locality,+fragile-hint-constr
522-
# Remove unsupported-attributes once we stop supporting < 8.14
523-
WARNINGS := $(WARNINGS_PLUS),unsupported-attributes
522+
WARNINGS := $(WARNINGS_PLUS),-deprecated-since-9.0,-deprecated-since-8.20,-deprecated-from-Coq
524523
COQPROJECT_CMD:=(echo '-R $(SRC_DIR) $(MOD_NAME)'; printf -- '$(DEPFLAGS_NL)'; echo '-arg -w -arg $(WARNINGS)'; echo '-arg -native-compiler -arg ondemand'; echo 'src/Everything.v'; echo 'src/Bedrock/Everything.v'; find src -type f -name '*.v' | $(GREP_EXCLUDE_SPECIAL) | $(GREP_EXCLUDE_GENERATED) | $(SORT_COQPROJECT))
525524
NEW_COQPROJECT_CONTENTS_SORTED:=$(shell $(COQPROJECT_CMD) | $(SORT_COQPROJECT))
526525

0 commit comments

Comments
 (0)