Typecheck pseudo sort poly inductives in kernel using above prop qvar #20102
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
SkySkimmer
added
kind: redesign
coqbot-app
bot
removed
the
request: full CI
SkySkimmer
added
the
request: full CI
SkySkimmer
force-pushed
the
kernel-template-qvar
branch
from
fe20f3c to
a3aadcc
Compare
coqbot-app
bot
removed
the
request: full CI
SkySkimmer
added
the
request: full CI
SkySkimmer
force-pushed
the
kernel-template-qvar
branch
from
a3aadcc to
99549c4
Compare
coqbot-app
bot
removed
the
request: full CI
SkySkimmer
added
the
request: full CI
SkySkimmer
force-pushed
the
kernel-template-qvar
branch
from
99549c4 to
9d450ce
Compare
coqbot-app
bot
removed
the
request: full CI
SkySkimmer
added
the
request: full CI
coqbot-app
bot
removed
the
request: full CI
SkySkimmer
added a commit
to SkySkimmer/MetaRocq
that referenced
this pull request
Jan 22, 2025
SkySkimmer
added
the
request: full CI
SkySkimmer
force-pushed
the
kernel-template-qvar
branch
from
a0d187e to
8b49777
Compare
coqbot-app
bot
removed
the
request: full CI
SkySkimmer
added
the
request: full CI
SkySkimmer
force-pushed
the
kernel-template-qvar
branch
from
8b49777 to
82c4d18
Compare
coqbot-app
bot
removed
the
request: full CI
ppedrot
approved these changes
Jan 23, 2025
Member
ppedrot
left a comment
ppedrot
left a comment
There was a problem hiding this comment.
This is increasing the level of hackishness of template-poly in the kernel, but since it's for the good cause I'm fine with it.
Member
|
@coqbot merge now |
Contributor
|
@ppedrot: Please take care of the following overlays:
|
ppedrot
added a commit
to MetaRocq/metarocq
that referenced
this pull request
Jan 23, 2025
Adapt to rocq-prover/rocq#20102 (template poly api change)
mattam82
added a commit
to MetaRocq/metarocq
that referenced
this pull request
Jan 29, 2025
This reverts commit 38a5a75.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Extracted from #19985
If the higher layers use sort polymorphism to infer template info they will send more general types to the kernel (typically
Inductive foo T := bar (_:nat -> T).will be inferred template) so the kernel needs to be modified, but the kernel change does not depend on the higher layer change AFAICT so we can make incremental progress here.Overlays: