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
Correct module document #15125
Correct module document #15125
Conversation
coq@3775df2 accidentally removed an overline.
"x" is not used in the rule.
The colon is added accidentally at coq@3775df2
The conclusion of WF-MOD2 was WF(E; Mod(X:S1[:=S2]))[]. But S2 should not be optional. In the case that S2 is not given here, WF-MOD2 is same as WF-MOD1 with meaningless premises for S2. coq@81f1219 changes the macro \Mod as: -\newcommand{\Mod}[3]{{\sf Mod}({coq#1}:{coq#2}:={coq#3})} +\newcommand{\Mod}[3]{{\sf Mod}({coq#1}:{coq#2}\,\zeroone{:={coq#3}})} So, "[" and "]" added in WF-MOD2 seems accidental.
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.
Looks good to me
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.
Thanks a lot, and sorry for the delay in handling this.
@coqbot merge now
By the way, @akr, we're aware that the section on modules is not the best organized in the Coq reference manual. So if you happen to have suggestions for larger changes, do not hesitate to propose them. |
I corrected several small problems in
doc/sphinx/language/core/modules.rst .