-
Notifications
You must be signed in to change notification settings - Fork 49
Expand file tree
/
Copy path_RocqProject
More file actions
20 lines (19 loc) · 878 Bytes
/
_RocqProject
File metadata and controls
20 lines (19 loc) · 878 Bytes
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
-Q src Perennial
-arg -w -arg +deprecated-instance-without-locality
# don't allow ambiguous coercions
-arg -w -arg +ambiguous-paths
-arg -w -arg +deprecated-hint-rewrite-without-locality
-arg -w -arg +deprecated-field-instance-without-locality
-arg -w -arg +deprecated-tactic-notation
# for coqutil compatibility
-arg -w -arg -deprecated-since-8.19,-deprecated-since-8.20
-arg -w -arg -deprecated-since-9.0,-deprecated-since-9.1,-deprecated-since-9.2
# false positives with our byte_string
-arg -w -arg -via-type-remapping,-via-type-mismatch
-arg -w -arg +deprecated-typeclasses-transparency-without-locality
# Iris-disabled warnings
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-notation-incompatible-prefix
-arg -w -arg -unknown-warning
# Rocq 9.2+alpha issues not fixed
-arg -w -arg -postfix-notation-not-level-1,-closed-notation-not-level-0
-Q new New