diff options
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). |