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.
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
Fixes #15451: incompletenesses in guard condition regarding cofix and primitive projections #15498
Fixes #15451: incompletenesses in guard condition regarding cofix and primitive projections #15498
Conversation
0a42adf
to
9026195
Compare
kernel/inductive.ml
Outdated
| Construct _ -> | ||
check_rec_call renv [] | ||
| Construct _ | CoFix _ -> | ||
check_rec_call renv stack | ||
(Term.applist (mkProj(Projection.unfold p,c), l)) | ||
| _ -> Exninfo.iraise exn |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why not make this explicit so we definitely don't forget any cases?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good question. We could but there are a lot of cases to add. Wondering what others would do themselves.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think that in the kernel at least, it is considered good practice to fully enumerate the constructors of constr
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I agree, the catch-all bit me once in the guard as well when we introduced primitive projections.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
OK, done.
9026195
to
359dafd
Compare
This one is fairly simple and there is little risk of anything going wrong, so let me assign and merge. |
@coqbot merge now |
(cherry picked from commit 359dafd)
…dition regarding cofix and primitive projections
Kind: Fix
Two issues:
cofix
was missing when detecting the presence of a potential iota-redex to reduceFixes #15451