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.FMap.fold has incorrect type #18635

Closed
SkySkimmer opened this issue Feb 7, 2024 · 0 comments · Fixed by #18649
Closed

Ltac2.FMap.fold has incorrect type #18635

SkySkimmer opened this issue Feb 7, 2024 · 0 comments · Fixed by #18649
Labels
kind: bug An error, flaw, fault or unintended behaviour. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Milestone
8.19.1

Comments

@SkySkimmer
Copy link
Contributor

Declared as ('k -> 'v -> 'acc) -> ('k, 'v) t -> 'acc -> 'acc but should be ('k -> 'v -> 'acc -> 'acc) -> ('k, 'v) t -> 'acc -> 'acc
@SkySkimmer SkySkimmer added kind: bug An error, flaw, fault or unintended behaviour. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. labels Feb 7, 2024
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Feb 8, 2024
@SkySkimmer
Enforce typing of external declarations
60c945e 
Fix coq#18553
Fix coq#18635
@SkySkimmer SkySkimmer mentioned this issue Feb 8, 2024
Closed
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Feb 9, 2024
@SkySkimmer
Ltac2: fix type of FMap.fold
39b3871 
Fix coq#18635
@SkySkimmer SkySkimmer mentioned this issue Feb 9, 2024
Merged
@coqbot-app coqbot-app bot added this to the 8.19.1 milestone Feb 9, 2024
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Feb 19, 2024
@SkySkimmer
Ltac2: fix type of FMap.fold
92f762d 
Fix coq#18635

(cherry picked from commit 39b3871)
louiseddp pushed a commit to louiseddp/coq that referenced this issue Feb 27, 2024
@SkySkimmer @louiseddp
Ltac2: fix type of FMap.fold
113b636 
Fix coq#18635
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. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Projects
None yet
Milestone
8.19.1
1 participant
@SkySkimmer