diff options
| author | Jasper Hugunin | 2020-07-26 16:46:31 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-13 08:24:10 -0700 |
| commit | 94efd6ebfba06d94ee5fdedbe13ea386b658ab46 (patch) | |
| tree | f4c6d8a62a6e256586701ddb6b2082e7d9f5902d /mathcomp | |
| parent | 43ac266e1e99cad08a9c291b99efcc7eddc244e7 (diff) | |
Be robust to a change in the default argument naming algorithm.
Overlay for coq/coq#12756, which changes the default argument name to
just `S` from `S0`. This change preserves the old name; switching instead
to use `S` may be preferable but introduces a potential impact on
downstream users of mathcomp.
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/poly.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index d21e690..e83bc09 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -1700,7 +1700,7 @@ Arguments rootP {R p x}. Arguments rootPf {R p x}. Arguments rootPt {R p x}. Arguments unity_rootP {R n z}. -Arguments polyOverP {R S0 addS kS p}. +Arguments polyOverP {R S0 addS kS p} : rename. Arguments polyC_inj {R} [x1 x2] eq_x12P. Arguments eq_poly {R n} [E1] E2 eq_E12. |