Skip to content
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

Make clear more powerful #716

Closed
sarranz opened this issue Feb 11, 2025 · 2 comments · Fixed by #713
Closed

Make clear more powerful #716

sarranz opened this issue Feb 11, 2025 · 2 comments · Fixed by #713

Comments

@sarranz
Copy link

sarranz commented Feb 11, 2025

It would be nice to have clear. remove everything in the context except what's needed for the goal to make sense, and also to be able to clear everything except some hypotheses, writing for instance clear - h0 h1..
@Cameron-Low Cameron-Low linked a pull request Feb 11, 2025 that will close this issue
Extend clear tactic to allow clearing *all* unused items in the context recursively #713
Merged
@Cameron-Low Cameron-Low mentioned this issue Feb 11, 2025
Merged
@fdupress
Copy link
Member

@sarranz , can you quickly give #713 a whirl and check that it behaves as you expect? Thanks!

@sarranz
Copy link
Author

sarranz commented Feb 12, 2025

I just tried it out, it behaves exactly as I expect, thanks a lot!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Extend clear tactic to allow clearing *all* unused items in the context recursively oskgo/easycrypt
2 participants
@fdupress @sarranz