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

"Inductive types with annotations not supported." is not documented #16762

Open
JasonGross opened this issue Nov 1, 2022 · 1 comment
Open

"Inductive types with annotations not supported." is not documented #16762

JasonGross opened this issue Nov 1, 2022 · 1 comment
Labels
kind: documentation Additions or improvement to documentation. kind: user messages Improvement of error messages, new warnings, etc.

Comments

@JasonGross
Copy link
Member

Description of the problem

coq/vernac/indschemes.ml

Lines 153 to 155 in 94e4e43

| DecidabilityIndicesNotSupported ->
alarm what internal
(str "Inductive types with annotations not supported.")

is not documented

What does it mean?

Coq Version

8.16
@JasonGross JasonGross added kind: documentation Additions or improvement to documentation. kind: user messages Improvement of error messages, new warnings, etc. labels Nov 1, 2022
@SkySkimmer
Copy link
Contributor

It should say indices instead of annotations

SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Apr 28, 2023
@SkySkimmer
Stop calling inductive indices "annotations" in the doc
2270faa 
cf also coq#16762
@SkySkimmer SkySkimmer mentioned this issue Apr 28, 2023
Merged
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: user messages Improvement of error messages, new warnings, etc.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@JasonGross @SkySkimmer