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

[vernac] Improve alpha-renaming in record projection types #13852

Merged
merged 1 commit into from
Mar 25, 2021
Merged

[vernac] Improve alpha-renaming in record projection types #13852

merged 1 commit into from
Mar 25, 2021

Conversation

Lysxia
Copy link
Contributor

@Lysxia Lysxia commented Feb 12, 2021 •
edited by SkySkimmer
Loading

Kind: feature

Closes #13727

Overlay: AbsInt/CompCert#388

@Lysxia
Copy link
Contributor Author

Lysxia commented Feb 12, 2021

Is there a better way of doing this?

@Lysxia Lysxia changed the title [kernel] Avoid name collisions in record projection types [vernac] Avoid name collisions in record projection types Feb 12, 2021
@Lysxia Lysxia changed the title [vernac] Avoid name collisions in record projection types [vernac] Improve alpha-renaming in record projection types Feb 12, 2021
@SkySkimmer
Copy link
Contributor

The compcert error is because of something like

Record nlalal := {
  x:nat;
  f : forall n:nat, n=x -> True
}.

Goal True.
  apply f with (n0:=0).

@SkySkimmer SkySkimmer added the needs: overlay This is breaking external developments we track in CI. label Feb 22, 2021
Lysxia added a commit to Lysxia/CompCert that referenced this pull request Mar 6, 2021
@Lysxia
Adapt to new projection parameter names (coq/coq#13852)
88989be
@Lysxia Lysxia mentioned this pull request Mar 6, 2021
Merged
@Lysxia Lysxia removed the needs: overlay This is breaking external developments we track in CI. label Mar 6, 2021
@Lysxia Lysxia marked this pull request as ready for review March 6, 2021 22:30
@Lysxia Lysxia requested a review from a team as a code owner March 6, 2021 22:30
Lysxia added a commit to Lysxia/CompCert that referenced this pull request Mar 6, 2021
@Lysxia
Adapt to new projection parameter names (coq/coq#13852)
6a0d1ad
@SkySkimmer SkySkimmer self-assigned this Mar 10, 2021
@SkySkimmer SkySkimmer added the kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. label Mar 10, 2021
@SkySkimmer SkySkimmer added this to the 8.14+rc1 milestone Mar 10, 2021
SkySkimmer
SkySkimmer approved these changes Mar 10, 2021
View reviewed changes
Copy link
Contributor

@SkySkimmer SkySkimmer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll wait for the overlay to be merged upstream before merging this.

xavierleroy pushed a commit to AbsInt/CompCert that referenced this pull request Mar 25, 2021
@Lysxia
Do not depend on projection parameter names (#388)
6106e04 
coq/coq#13852 fixes an oddity in the automatically-generated names for projection parameters.
There was one place in CompCert where one of these automatically-generated names was used.
This commit avoids using this name.
@SkySkimmer
Copy link
Contributor

@coqbot: merge now

@coqbot-app coqbot-app bot merged commit 1e1a72f into coq:master Mar 25, 2021
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Mar 25, 2021

@SkySkimmer: Please take care of the following overlays:

  • 13852-Lysxia-no-collision-projection.sh

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc.
Projects
None yet
Milestone
8.14+rc1
Development

Successfully merging this pull request may close these issues.

Avoid alpha-renaming in projection types
2 participants
@Lysxia @SkySkimmer