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

Fix MetaCoq utils imports #233

Merged
merged 1 commit into from
Oct 24, 2023
Merged

Fix MetaCoq utils imports #233

merged 1 commit into from
Oct 24, 2023

Conversation

4ever2
Copy link
Collaborator

@4ever2 4ever2 commented Oct 16, 2023

Building fails when coq-metacoq-quotation is installed because the import statement From MetaCoq Require Import utils isn't specific enough.

@4ever2 4ever2 added type: bug Something isn't working part: embedding Issues and PRs related to the embedding layer labels Oct 16, 2023
@4ever2 4ever2 merged commit af5318c into AU-COBRA:master Oct 24, 2023
2 checks passed
@4ever2 4ever2 deleted the fix-imports branch October 24, 2023 08:42
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
part: embedding Issues and PRs related to the embedding layer type: bug Something isn't working
Projects
None yet
Milestone
No milestone
Development

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