diff options
| author | Kazuhiko Sakaguchi | 2021-01-05 19:46:05 +0900 |
|---|---|---|
| committer | GitHub | 2021-01-05 19:46:05 +0900 |
| commit | 58c3ed3e5f038ef815f0cdd19ac0914fe47eb300 (patch) | |
| tree | ac8fcee9ab622c09939b5f55a190df3cd3a8f25b | |
| parent | ee410eb85f36f5e366f807207a7dee8f3e1bdf3a (diff) | |
| parent | 92efd5efceb6835523e0bb2d09cd12e3b21a4127 (diff) | |
Merge pull request #690 from affeldt-aist/erroneous_warning
erroneous deprecation warning
| -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). |