Skip to content

Support generalized rewriting in let bindings#20985

Open
mattam82 wants to merge 1 commit into
rocq-prover:masterfrom
mattam82:rewrite-in-lets
Open

Support generalized rewriting in let bindings#20985
mattam82 wants to merge 1 commit into
rocq-prover:masterfrom
mattam82:rewrite-in-lets

Conversation

@mattam82

@mattam82 mattam82 commented Jul 31, 2025

Copy link
Copy Markdown
Member

Fixes / closes #????

  • Added / updated test-suite.
  • Added changelog.

@coqbot-app coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jul 31, 2025
@mattam82 mattam82 marked this pull request as ready for review February 5, 2026 15:39
@mattam82 mattam82 requested a review from a team as a code owner February 5, 2026 15:39
@SkySkimmer SkySkimmer self-assigned this Feb 5, 2026
Comment thread tactics/rewrite.ml
Comment thread tactics/rewrite.ml Outdated
@mattam82 mattam82 requested a review from a team as a code owner February 5, 2026 15:58
@ppedrot ppedrot added the needs: merge of dependency This PR depends on another PR being merged first. label Feb 15, 2026
@mattam82

Copy link
Copy Markdown
Member Author

@coqbot run full ci

@coqbot-app coqbot-app Bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Feb 15, 2026
@mattam82

Copy link
Copy Markdown
Member Author

@coqbot bench

@SkySkimmer SkySkimmer added needs: fixing The proposed code change is broken. and removed needs: merge of dependency This PR depends on another PR being merged first. labels Feb 17, 2026
@SkySkimmer

Copy link
Copy Markdown
Contributor

It seems like it timed out in PString?

@coqbot-app coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Feb 17, 2026
@SkySkimmer

Copy link
Copy Markdown
Contributor

@coqbot run full ci

@coqbot-app coqbot-app Bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Feb 18, 2026
@SkySkimmer SkySkimmer removed the needs: fixing The proposed code change is broken. label Feb 18, 2026
@coqbot-app

coqbot-app Bot commented Feb 18, 2026

Copy link
Copy Markdown
Contributor

🔴 CI failures at commit 37c239a without any failure in the test-suite

✔️ Corresponding jobs for the base commit 00937db succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-coq_performance_tests, ci-math_classes
  • You can also pass me a specific list of targets to minimize as arguments.

@mattam82

Copy link
Copy Markdown
Member Author

@coqbot run full ci

@SkySkimmer SkySkimmer added the kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. label Feb 25, 2026
@SkySkimmer SkySkimmer added this to the 9.3+rc1 milestone Feb 25, 2026
@SkySkimmer

Copy link
Copy Markdown
Contributor

@coqbot run full ci

@SkySkimmer SkySkimmer added the needs: overlay This is breaking external developments we track in CI. label Feb 25, 2026
@coqbot-app

coqbot-app Bot commented Feb 25, 2026

Copy link
Copy Markdown
Contributor

🔴 CI failures at commit 37c239a without any failure in the test-suite

✔️ Corresponding jobs for the base commit c4fa328 succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-coq_performance_tests, ci-math_classes
  • You can also pass me a specific list of targets to minimize as arguments.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. needs: overlay This is breaking external developments we track in CI.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants