Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Renaming arguments in nested sections #18392

Closed
herbelin opened this issue Dec 9, 2023 · 2 comments · Fixed by #18393
Closed

Renaming arguments in nested sections #18392

herbelin opened this issue Dec 9, 2023 · 2 comments · Fixed by #18393
Labels
kind: bug An error, flaw, fault or unintended behaviour. kind: user messages Improvement of error messages, new warnings, etc. part: implicit arguments The implicit arguments mechanism, generalizable variables, etc. part: sections The section mechanism of Coq.
Milestone
8.19+rc1

Comments

@herbelin
Copy link
Member

herbelin commented Dec 9, 2023

Description of the problem

A small bug in situations where Arguments renames arguments in nested sections:

Section S.
Variable a : nat.
Section T.
Variable b : nat.
Axiom f : forall c, a + b = c.
Global Arguments f c' : rename.
About f. (* f : forall c' : nat, a + b = c' *)
End T.
About f. (* forall b c' : nat, a + b = c' *)
End S.
About f. (* f : forall a c' c : nat, a + c' = c *)

I'll do a fix.

Coq Version

Since the beginning of Arguments (8.4).
@herbelin herbelin added kind: user messages Improvement of error messages, new warnings, etc. part: sections The section mechanism of Coq. kind: bug An error, flaw, fault or unintended behaviour. part: implicit arguments The implicit arguments mechanism, generalizable variables, etc. labels Dec 9, 2023
@herbelin herbelin added this to the 8.20+rc1 milestone Dec 9, 2023
herbelin added a commit to herbelin/github-coq that referenced this issue Dec 9, 2023
@herbelin
Fixing coq#18392: argument names missing in nested sections.
c1e69dc
@herbelin
Copy link
Member Author

herbelin commented Dec 9, 2023

Was actually already reported as #12755.

herbelin added a commit to herbelin/github-coq that referenced this issue Dec 9, 2023
@herbelin
Fixing coq#18392: argument names missing in nested sections.
7de5207
@herbelin herbelin mentioned this issue Dec 9, 2023
Merged
2 tasks
herbelin added a commit to herbelin/github-coq that referenced this issue Dec 9, 2023
@herbelin
Fixing coq#12755 and coq#18392: argument names wrongly shifted in nes…
84a1310 
…ted sections.
herbelin added a commit to herbelin/github-coq that referenced this issue Dec 10, 2023
@herbelin
Fixing coq#12755 and coq#18392: argument names wrongly shifted in nes…
0159fff 
…ted sections.
coqbot-app bot added a commit that referenced this issue Dec 11, 2023
@coqbot-app @SkySkimmer
Merge PR #18393: Fixes #12755 and #18392: argument names wrongly shif…
3a8c562 
…ted in nested sections

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Dec 11, 2023

The milestone of this issue was changed to reflect the one of the pull request that closed it.

@coqbot-app coqbot-app bot modified the milestones: 8.20+rc1, 8.19+rc1 Dec 11, 2023
SkySkimmer pushed a commit to SkySkimmer/coq that referenced this issue Dec 13, 2023
@herbelin @SkySkimmer
Fixing coq#12755 and coq#18392: argument names wrongly shifted in nes…
fab776d 
…ted sections.

(cherry picked from commit 84a1310)
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Dec 13, 2023
@SkySkimmer
Backport PR coq#18393: Fixes coq#12755 and coq#18392: argument names …
b2ba41f 
…wrongly shifted in nested sections
SkySkimmer pushed a commit that referenced this issue Dec 14, 2023
@herbelin @SkySkimmer
Fixing #12755 and #18392: argument names wrongly shifted in nested se…
917b54b 
…ctions.

(cherry picked from commit 84a1310)
SkySkimmer added a commit that referenced this issue Dec 14, 2023
@SkySkimmer
Backport PR #18393: Fixes #12755 and #18392: argument names wrongly s…
0cde3fb 
…hifted in nested sections
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: bug An error, flaw, fault or unintended behaviour. kind: user messages Improvement of error messages, new warnings, etc. part: implicit arguments The implicit arguments mechanism, generalizable variables, etc. part: sections The section mechanism of Coq.
Projects
None yet
Milestone
8.19+rc1
Development

Successfully merging a pull request may close this issue.

Fixes #12755 and #18392: argument names wrongly shifted in nested sections herbelin/github-coq
1 participant
@herbelin