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.

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

Extend clear tactic to allow clearing *all* unused items in the context recursively #713

Merged
merged 1 commit into from
Feb 21, 2025

Conversation

oskgo
Copy link
Contributor

@oskgo oskgo commented Feb 10, 2025

This feature was requested at the retreat.

Please have patience with the review. This is literally the first OCaml code I've ever written.

@Cameron-Low Cameron-Low linked an issue Feb 11, 2025 that may be closed by this pull request
@Cameron-Low
Copy link
Contributor

As a first thing: it is probably best to add a unit test for this. There are a few examples in the ./tests folder if you need some inspiration. Secondly, there’s #716 that we should make sure is fully addressed.

@oskgo oskgo changed the title Add clear * tactic to clear all unused items in the context recursively Extend clear tactic to allow clearing *all* unused items in the context recursively Feb 12, 2025
@oskgo
Copy link
Contributor Author

oskgo commented Feb 12, 2025

I've made the syntax change and feature additions as requested, and also added a test.

Copy link
Contributor

@Cameron-Low Cameron-Low left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just a few nits on style, otherwise looks good to me.

Copy link
Contributor

@Cameron-Low Cameron-Low left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

all good from me. @strub anything you want to add?

@strub
Copy link
Member

strub commented Feb 19, 2025

When you are done, could you squash your commits into one?

@oskgo
Copy link
Contributor Author

oskgo commented Feb 20, 2025

All done and squashed

@fdupress
Copy link
Member

We can flag this as fixing #716 when merging.

@strub strub self-assigned this Feb 21, 2025
@strub strub merged commit 7e6bf73 into EasyCrypt:main Feb 21, 2025
15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Make clear more powerful
4 participants