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

Declare universe variables in Context commands #1781

Merged
merged 1 commit into from
Oct 10, 2023

Conversation

jdchristensen
Copy link
Collaborator

I searched the library and only found one more place where a universe variable was used in a Context command without being declared. I also found an out-of-date comment, which only was relevant if the universe variable in question was not declared.

@Alizter
Copy link
Collaborator

Alizter commented Oct 10, 2023

Feel free to merge.

@jdchristensen jdchristensen merged commit 8deb346 into HoTT:master Oct 10, 2023
23 checks passed
@jdchristensen jdchristensen deleted the universes_in_context branch October 10, 2023 18:46
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