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

Add From coqutil to imports #128

Merged
merged 2 commits into from
Mar 6, 2025
Merged

Conversation

tchajed
Copy link
Contributor

@tchajed tchajed commented Mar 6, 2025

Perennial builds coqutil with a _CoqProject that uses -Q coqutil/src coqutil rather than -R, which makes these From coqutil qualifiers required.

We could change Perennial but I think these are good style anyway and this is the first time this has been a problem.

@samuelgruetter
Copy link
Contributor

samuelgruetter commented Mar 6, 2025

I'm surprised we don't use -Q in our own (generated) _CoqProject, which would have caught these non-qualified imports (probably introduced in #127). So I pushed the -R to -Q change right to the branch of this PR

@samuelgruetter samuelgruetter merged commit 4597335 into mit-plv:master Mar 6, 2025
2 checks passed
@tchajed tchajed deleted the from-require branch March 6, 2025 18:32
@tchajed
Copy link
Contributor Author

tchajed commented Mar 6, 2025

Awesome, thanks for the fast response and fixing the underlying issue, too.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants