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

Support syntax Type@{q | _} #18981

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Support syntax Type@{q | _} #18981

wants to merge 1 commit into from

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Apr 26, 2024 •
edited

@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 26, 2024
@SkySkimmer SkySkimmer requested review from a team as code owners April 26, 2024 12:35
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 26, 2024
SkySkimmer added a commit to SkySkimmer/autosubst-ocaml that referenced this pull request Apr 29, 2024
@SkySkimmer
Adapt to coq/coq#18981 (universe syntax change)
0f6b7db
SkySkimmer added a commit to SkySkimmer/coq-elpi that referenced this pull request Apr 29, 2024
@SkySkimmer
Adapt to coq/coq#18981 (universe syntax change)
6353fe8
@SkySkimmer SkySkimmer added kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. request: full CI Use this label when you want your next push to trigger a full CI. part: universes The universe system. labels Apr 29, 2024
@SkySkimmer SkySkimmer added this to the 8.20+rc1 milestone Apr 29, 2024
@SkySkimmer SkySkimmer added part: sort polymorphism The sorts subsystem of the universe system. part: parser labels Apr 29, 2024
SkySkimmer added a commit to SkySkimmer/QuickChick that referenced this pull request Apr 29, 2024
@SkySkimmer
Adapt to coq/coq#18981 (universe syntax change)
c739407
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 29, 2024
@ppedrot ppedrot self-assigned this Apr 30, 2024
jfehrle

This comment was marked as off-topic.

Sign in to view

jfehrle
jfehrle reviewed May 3, 2024
View reviewed changes
doc/sphinx/language/core/sorts.rst
@@ -19,6 +19,7 @@ Sorts
| Type @%{ _ %}
| Type @%{ {? @qualid %| } @universe %}
universe ::= max ( {+, @universe_expr } )
| _
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should there be some explanation of what this production does?

@jfehrle jfehrle added the needs: changelog entry This should be documented in doc/changelog. label May 3, 2024
@SkySkimmer SkySkimmer removed the needs: changelog entry This should be documented in doc/changelog. label May 7, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jfehrle jfehrle jfehrle left review comments

At least 1 approving review is required to merge this pull request.

Assignees

@ppedrot ppedrot

Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: parser part: sort polymorphism The sorts subsystem of the universe system. part: universes The universe system.
Projects
None yet
Milestone
8.20+rc1
Development

Successfully merging this pull request may close these issues.

Unspecified universe levels (_) trigger a syntax error in Type with sort variables
3 participants
@SkySkimmer @jfehrle @ppedrot