diff options
| author | Jasper Hugunin | 2020-08-19 08:13:08 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-19 08:13:08 -0700 |
| commit | 300157fc6176856f3f792d956925af366ef3329e (patch) | |
| tree | 081a7e7c5f2cd86f74fe2282f66d9cc79a4f35cc /dev | |
| parent | 55f4095fe3c366a9f310584a55e2dc0605e5409c (diff) | |
Do not refresh the names of implicit arguments.
Try just going with the user-given names, and not worrying about
what happens with repeated names or anonymous implicits.
(Support for anonymous implicits is due to herbelin in #11098.)
This PR should not change behaviour in the absence of repeated names.
Since repeated names are already a poorly handled corner case, I would
recommend changing binder names to avoid overlap in the case of a
change in behavior.
Since anonymous implicits and implicits with repeated names can already
happen, I think this is unlikely to cause too many new problems,
though it might exacerbate existing ones. However, I already had to fix
one newly possible anomaly, so I can't be too confident.
The most common change in external developments was that an argument
no longer gets `0` appended to it, causing the `Arguments` command
to complain about renaming.
To fix this and keep the old name, one can simply use the `rename` flag
as suggested, or switch to the new, un-suffixed name.
Closes #6785
Closes #12001
Another step towards checking the standard library with `-mangle-names`.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh b/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh new file mode 100644 index 0000000000..54fdd87566 --- /dev/null +++ b/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "12756" ] || [ "$CI_BRANCH" = "dont-refresh-argument-names" ]; then + + mathcomp_CI_REF=dont-refresh-argument-names-overlay + mathcomp_CI_GITURL=https://github.com/jashug/math-comp + + oddorder_CI_REF=dont-refresh-argument-names-overlay + oddorder_CI_GITURL=https://github.com/jashug/odd-order + +fi |