Make a PR to the main library including WildCat/Square

mikeshulman / Coq-HoTT

Homotopy type theory

http://homotopytypetheory.org/

Other

12 stars 4 forks source link

Make a PR to the main library including WildCat/Square #38

Closed mikeshulman closed 4 years ago

mikeshulman commented 4 years ago

Every time I switch from the wildcat branch to the master branch, the leftover compiled WildCat/Square.vo gets mistakenly imported by Cubical/DSquare until I delete it. Let's at least merge a change that will stop that from happening.

First we'll have to merge master back into wildcat, which will require a bit of manual work.

Alizter commented 4 years ago

Or we make a PR to the main library implementing the naming changes in the cubical library. I don't think WildCat/Square is ready to merged into the main library yet. For one, we need to agree on a naming convention.