Skip to content

Don't check opacity of constant in Typeclasses Opaque#21669

Open
SkySkimmer wants to merge 3 commits intorocq-prover:masterfrom
SkySkimmer:eval-ref
Open

Don't check opacity of constant in Typeclasses Opaque#21669
SkySkimmer wants to merge 3 commits intorocq-prover:masterfrom
SkySkimmer:eval-ref

Conversation

@SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Feb 24, 2026 •
edited
Loading

@SkySkimmer SkySkimmer requested review from a team as code owners February 24, 2026 15:49
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 24, 2026
@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 Feb 24, 2026
@ppedrot ppedrot self-assigned this Feb 25, 2026
@ppedrot ppedrot added this to the 9.3+rc1 milestone Feb 25, 2026
@ppedrot ppedrot added kind: fix This fixes a bug or incorrect documentation. needs: overlay This is breaking external developments we track in CI. labels Feb 25, 2026
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: overlay This is breaking external developments we track in CI. labels Feb 26, 2026
@SkySkimmer SkySkimmer requested review from a team as code owners February 26, 2026 14:07
@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 Feb 26, 2026
@ppedrot
Copy link
Member

ppedrot commented Feb 27, 2026

Something is wrong with the CI, you should probably rebase the overlays and the PR to get a clean run.

@SkySkimmer SkySkimmer added the needs: overlay This is breaking external developments we track in CI. label Feb 27, 2026
SkySkimmer added a commit to SkySkimmer/MetaRocq that referenced this pull request Feb 27, 2026
@SkySkimmer
Adapt to rocq-prover/rocq#21669 (evaluable_of_global_reference no env…
5840bac 
… arg)
SkySkimmer added a commit to SkySkimmer/rewriter that referenced this pull request Feb 27, 2026
@SkySkimmer
Adapt to rocq-prover/rocq#21669 (evaluable_of_global_reference no env…
0749957 
… arg)
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: overlay This is breaking external developments we track in CI. labels Feb 27, 2026
@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 Feb 27, 2026
SkySkimmer added a commit to SkySkimmer/rewriter that referenced this pull request Feb 27, 2026
@SkySkimmer
Adapt to rocq-prover/rocq#21669 (evaluable_of_global_reference no env…
4e9dc8d 
… arg)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels

kind: fix This fixes a bug or incorrect documentation.

Projects

None yet

Milestone

9.3+rc1

Development

Successfully merging this pull request may close these issues.

Typeclasses Opaque fails on Opaque definitions

2 participants

@SkySkimmer @ppedrot