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

introduce a "coercion class" glossary definition #15680

Open
Alizter opened this issue Feb 14, 2022 · 0 comments
Open

introduce a "coercion class" glossary definition #15680

Alizter opened this issue Feb 14, 2022 · 0 comments
Labels
kind: documentation Additions or improvement to documentation. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc.
Projects
User documentation

Comments

@Alizter
Copy link
Contributor

Alizter commented Feb 14, 2022 •
edited by jfehrle

This is unrelated to the PR, but it would be great to introduce a "coercion class" glossary definition and to use it here. (Class may mean several things in Coq, type class / coercion class, and thus using :term:`class <coercion class>` may help disambiguate (even though here the context can help too).

Originally posted by @Zimmi48 in #15489 (comment)
@Alizter Alizter added kind: documentation Additions or improvement to documentation. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. labels Feb 14, 2022
@Alizter Alizter mentioned this issue Feb 14, 2022
Merged
1 task
@Alizter Alizter added this to Writing in User documentation May 17, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: documentation Additions or improvement to documentation. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc.
Projects
User documentation
Status: Writing
User documentation
  
Writing
Milestone
No milestone
Development

No branches or pull requests
1 participant
@Alizter