Skip to content

Don't ignore undeclared-scope warnings #51

New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

#

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Jump to bottom
Merged
merged 1 commit into from
Jan 31, 2020
Merged

Don't ignore undeclared-scope warnings #51

merged 1 commit into from
Jan 31, 2020

Conversation

anton-trunov
Copy link
Member

@anton-trunov anton-trunov commented Jan 31, 2020 •
edited
Loading

With Coq 8.11 out we can finally fix #28. I used templates/generate.sh to regenerate README.md, the opam file, etc.

@anton-trunov anton-trunov force-pushed the fix-undeclared-scope-warnings branch 3 times, most recently from b72558d to 32e9f38 Compare January 31, 2020 10:17
@anton-trunov anton-trunov requested a review from palmskog January 31, 2020 10:19
@anton-trunov anton-trunov force-pushed the fix-undeclared-scope-warnings branch 3 times, most recently from 7c53909 to 6aace61 Compare January 31, 2020 11:50
@anton-trunov anton-trunov force-pushed the fix-undeclared-scope-warnings branch from 6aace61 to 1a21e62 Compare January 31, 2020 11:57
@anton-trunov anton-trunov merged commit 88deb0a into master Jan 31, 2020
@anton-trunov anton-trunov deleted the fix-undeclared-scope-warnings branch January 31, 2020 12:09
# for free to join this conversation on GitHub. Already have an account? # to comment
Reviewers

@palmskog palmskog Awaiting requested review from palmskog

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Fix undeclared scope warnings
1 participant
@anton-trunov