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

changed '@D' notation to '@Dp' #1439

Merged

andreaslyn merged 1 commit into HoTT:master from Alizter:notation-quickfix

Apr 2, 2021

Collaborator

Alizter commented Apr 2, 2021

fixes #1437


          changed '@d' notation to '@dp'

b6267d2

Alizter added bugfix cleanup notation labels

Collaborator Author

Alizter commented Apr 2, 2021

Whoops github seems to have pinged some random users.

Contributor

mikeshulman commented Apr 2, 2021

Looks ok, I guess.

andreaslyn merged commit a21f4df into HoTT:master

Alizter deleted the notation-quickfix branch

May 19, 2021 00:39

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bugfix cleanup notation