aboutsummaryrefslogtreecommitdiff
path: root/.github/pull_request_template.md
diff options
context:
space:
mode:
authorJasper Hugunin2020-07-26 16:46:31 -0700
committerJasper Hugunin2020-08-13 08:24:10 -0700
commit94efd6ebfba06d94ee5fdedbe13ea386b658ab46 (patch)
treef4c6d8a62a6e256586701ddb6b2082e7d9f5902d /.github/pull_request_template.md
parent43ac266e1e99cad08a9c291b99efcc7eddc244e7 (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 '.github/pull_request_template.md')
0 files changed, 0 insertions, 0 deletions