Make sure that you have [hoqc](https://github.com/HoTT/HoTT) installed. Then generate
the Makefile and build the project:
coq_makefile -f _CoqProject -o Makefile
make
Reference in New Issue
Block a user
Blocking a user prevents them from interacting with repositories, such as opening or commenting on pull requests or issues. Learn more about blocking a user.