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
Code cleanup in notations: use records instead of tuples for entries and subentries #17823
Code cleanup in notations: use records instead of tuples for entries and subentries #17823
Conversation
…tuples. See comment at coq#17117 (comment).
0b9986c
to
99ed573
Compare
type notation_entry_level = { | ||
notation_entry : notation_entry; | ||
notation_level : entry_level; | ||
} |
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.
@herbelin if you have the energy, the form:
module Entry_level = struct
type t = { entry : notation_entry;
; level : entry_level
}
end
tends to work better.
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 don't buy the "; ..." formatting which moreover is not the most "standard" way to format records in the code of Coq.
Otherwise, what are the pros and cons of using a module? And how do you measure the "better"?
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.
Using a module only makes sense if you have functions directly related to it together. If it is just a one off type its probably not worth it.
@coqbot run full ci |
The job library:ci-fiat_crypto_legacy has failed in allow failure mode |
@coqbot merge now |
@proux01: Please take care of the following overlays:
|
This was suggested by @proux01 in this comment of #17117 and this makes explicit when entries (equivalent of
in entry at level nn
) and subentries (equivalent ofid entry at level nn
) matter in the code.No semantic change.
Overlay: