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

Merged
merged 1 commit into from May 16, 2024
Merged

Support syntax Type@{q | _} #18981

merged 1 commit into from May 16, 2024

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
@ppedrot
Copy link
Member

ppedrot commented May 16, 2024

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 8bb85a9 into coq:master May 16, 2024
6 checks passed
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented May 16, 2024

@ppedrot: Please take care of the following overlays:

  • 18981-SkySkimmer-sort-expr-anon-univ.sh

ppedrot added a commit to LPCIC/coq-elpi that referenced this pull request May 16, 2024
@ppedrot
Merge pull request #623 from SkySkimmer/sort-expr-anon-univ
7a36cc8 
Adapt to coq/coq#18981 (universe syntax change)
@SkySkimmer SkySkimmer deleted the sort-expr-anon-univ branch May 16, 2024 14:07
liyishuai pushed a commit to SkySkimmer/QuickChick that referenced this pull request May 16, 2024
@SkySkimmer @liyishuai
Adapt to coq/coq#18981 (universe syntax change)
194558b
liyishuai pushed a commit to QuickChick/QuickChick that referenced this pull request May 17, 2024
@SkySkimmer @liyishuai
Adapt to coq/coq#18981 (universe syntax change)
4aacf02
yforster pushed a commit to uds-psl/autosubst-ocaml that referenced this pull request May 21, 2024
@SkySkimmer
Adapt to coq/coq#18981 (universe syntax change) (#15)
830b3d6
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

@ppedrot ppedrot ppedrot approved these changes

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 @ppedrot @jfehrle