Skip to content

Commit e0dbd6f

Browse files
committed
Uncomment warning as error
1 parent 9d7ea6e commit e0dbd6f

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

_CoqProject

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,4 +39,5 @@ theories/wielandt_fixpoint.v
3939
-arg -w -arg -redundant-canonical-projection
4040
-arg -w -arg -notation-overridden
4141
# introduced in Rocq 9.2
42-
-arg -w -arg +level-tolerance
42+
# Uncomment when https://github.com/math-comp/math-comp/pull/1110 gets merged
43+
# -arg -w -arg +level-tolerance

0 commit comments

Comments
 (0)