diff options
| author | Reynald Affeldt | 2021-01-04 13:56:16 +0900 |
|---|---|---|
| committer | Reynald Affeldt | 2021-01-04 13:56:16 +0900 |
| commit | 92efd5efceb6835523e0bb2d09cd12e3b21a4127 (patch) | |
| tree | ac8fcee9ab622c09939b5f55a190df3cd3a8f25b /mathcomp | |
| parent | ee410eb85f36f5e366f807207a7dee8f3e1bdf3a (diff) | |
erroneous deprecation warning
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/polydiv.v | 2 |
1 files changed, 1 insertions, 1 deletions
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). |