Skip to content

Remove bugged Loose Hint Behavior and fix incorrect Import optim #20698

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
Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Remove bugged Loose Hint Behavior and fix incorrect Import optim #20698

wants to merge 3 commits into from

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Jun 2, 2025 •
edited
Loading

@SkySkimmer SkySkimmer requested review from a team as code owners June 2, 2025 13:42
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Jun 2, 2025
@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 2, 2025
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Jun 2, 2025
@SkySkimmer SkySkimmer requested a review from a team as a code owner June 2, 2025 13:45
@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 2, 2025
@Villetaneuse Villetaneuse removed the request for review from a team June 3, 2025 15:33
@SkySkimmer
Remove bugged Loose Hint Behavior and fix incorrect Import optim
095709b 
Test case from rocq-prover#20695

AFAICT he Loose Hint Behavior option did nothing since
245b94c
(where load_function stopped loading non-superglobal Add Hints)
SkySkimmer added a commit to SkySkimmer/coq-waterproof that referenced this pull request Jun 5, 2025
@SkySkimmer
Adapt to rocq-prover/rocq#20698 (removed wrap_hint_warning)
6a3d130
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Jun 5, 2025
@SkySkimmer
Cleanup noop hint_warning functions
6e36101 
Since we never put nonempty data in the hint_trace these functions
never do anything.
@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 5, 2025
@SkySkimmer SkySkimmer added this to the 9.1+rc1 milestone Jun 5, 2025
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Jun 5, 2025
@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 5, 2025
@SkySkimmer SkySkimmer modified the milestones: 9.1+rc1, 9.2+rc1 Jun 12, 2025
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
None yet
Projects
None yet
Milestone
9.2+rc1
Development

Successfully merging this pull request may close these issues.
1 participant
@SkySkimmer