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

Ltac2 should support weak reduction flag #18209

Closed
SkySkimmer opened this issue Oct 25, 2023 · 0 comments · Fixed by #18273
Closed

Ltac2 should support weak reduction flag #18209

SkySkimmer opened this issue Oct 25, 2023 · 0 comments · Fixed by #18273
Labels
kind: wish Feature or enhancement requests. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Milestone
8.19+rc1

Comments

@SkySkimmer
Copy link
Contributor

from #17503

This requires some backwards incompatibility since the red_flags record needs to have a new field.
@SkySkimmer SkySkimmer added part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. kind: wish Feature or enhancement requests. labels Oct 25, 2023
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Nov 7, 2023
@SkySkimmer
Ltac2: support "head" reduction flag
fcf4ed7 
Close coq#18209
@SkySkimmer SkySkimmer mentioned this issue Nov 7, 2023
Merged
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Nov 8, 2023
@SkySkimmer
Ltac2: support "head" reduction flag
9b55fbb 
Close coq#18209
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Nov 8, 2023
@SkySkimmer
Ltac2: support "head" reduction flag
33b30c9 
Close coq#18209
@coqbot-app coqbot-app bot added this to the 8.19+rc1 milestone Nov 15, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: wish Feature or enhancement requests. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Projects
None yet
Milestone
8.19+rc1
Development

Successfully merging a pull request may close this issue.

Ltac2: support "head" reduction flag SkySkimmer/coq
1 participant
@SkySkimmer