From e0dbd6f7776713665941e5c3e9e5ae792e382caf Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Jul 2025 16:23:26 +0200 Subject: [PATCH] Uncomment warning as error --- _CoqProject | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/_CoqProject b/_CoqProject index 0708acb..414c65a 100644 --- a/_CoqProject +++ b/_CoqProject @@ -39,4 +39,5 @@ theories/wielandt_fixpoint.v -arg -w -arg -redundant-canonical-projection -arg -w -arg -notation-overridden # introduced in Rocq 9.2 --arg -w -arg +level-tolerance +# Uncomment when https://github.com/math-comp/math-comp/pull/1110 gets merged +# -arg -w -arg +level-tolerance