Skip to content

Don't print term with minimized universes in Check/Eval#21949

Open
SkySkimmer wants to merge 4 commits into
rocq-prover:masterfrom
SkySkimmer:eval-noker
Open

Don't print term with minimized universes in Check/Eval#21949
SkySkimmer wants to merge 4 commits into
rocq-prover:masterfrom
SkySkimmer:eval-noker

Conversation

@SkySkimmer

@SkySkimmer SkySkimmer commented Apr 23, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Close #20508

Not sure I really like the output though, it seems pretty verbose.

@SkySkimmer SkySkimmer added kind: user messages Error messages, warnings, etc. request: full CI Use this label when you want your next push to trigger a full CI. labels Apr 23, 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 Apr 23, 2026
@yannl35133

yannl35133 commented Apr 23, 2026

Copy link
Copy Markdown
Contributor

Why do you print the ustate and not the "sort_context_set"?

@SkySkimmer

SkySkimmer commented Apr 23, 2026

Copy link
Copy Markdown
Contributor Author

I reused Show Universes to get outut about the pre-minimize and post-minimize ustate but maybe that's not the right thing to do

@SkySkimmer SkySkimmer added the needs: progress Work in progress: awaiting action from the author. label Apr 24, 2026
@github-actions github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Apr 30, 2026
@coqbot-app

coqbot-app Bot commented Jun 1, 2026

Copy link
Copy Markdown
Contributor

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

@coqbot-app coqbot-app Bot added the stale This PR will be closed unless it is rebased. label Jun 1, 2026
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: progress Work in progress: awaiting action from the author. labels Jun 15, 2026
@coqbot-app coqbot-app Bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. stale This PR will be closed unless it is rebased. request: full CI Use this label when you want your next push to trigger a full CI. labels Jun 15, 2026
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Jun 15, 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 Jun 15, 2026
@SkySkimmer

SkySkimmer commented Jun 15, 2026

Copy link
Copy Markdown
Contributor Author

should look better now

@SkySkimmer SkySkimmer marked this pull request as ready for review June 15, 2026 12:04
@SkySkimmer SkySkimmer requested review from a team as code owners June 15, 2026 12:04
@SkySkimmer SkySkimmer added this to the 9.3+rc1 milestone Jun 15, 2026
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Jun 16, 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 Jun 16, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

kind: user messages Error messages, warnings, etc.

Projects

None yet

Milestone

9.3+rc1

Development

Successfully merging this pull request may close these issues.

When T is sort-polymorphic, "Check @T" specializes the sort of T

2 participants

@SkySkimmer @yannl35133