From 92efd5efceb6835523e0bb2d09cd12e3b21a4127 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt
Date: Mon, 4 Jan 2021 13:56:16 +0900
Subject: erroneous deprecation warning

---
 mathcomp/algebra/polydiv.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v
index 8459c45..41147fb 100644
--- a/mathcomp/algebra/polydiv.v
+++ b/mathcomp/algebra/polydiv.v
@@ -3205,7 +3205,7 @@ Notation "@ 'divp_scalel'" :=
 Notation "@ 'divp_scaler'" :=
   (deprecate modp_scaler divpZr) (at level 10, only parsing) : fun_scope.
 Notation "@ 'divp_opp'" :=
-  (deprecate modp_opp divpN) (at level 10, only parsing) : fun_scope.
+  (deprecate divp_opp divpN) (at level 10, only parsing) : fun_scope.
 Notation "@ 'divp_add'" :=
   (deprecate modp_add divpD) (at level 10, only parsing) : fun_scope.
 Notation modp_scalel := (@modp_scalel _) (only parsing).
-- 
cgit v1.2.3