zstone1

Excellent, glad you can repro. I don't have any critical timeline issues here. I have a workaround make file which will keep me unblocked for now. Thanks for the quick...

I encountered a possibly similar issue where a stray `.vo` file confusing the build. Doing a `make clean` doesn't remove `.vo` that correspond to deleted `.v` files. So you might...

Hm, removing the term `mixin` does make some sense in that the distinction between `mixin` and `factory` is a bit irrelevant to someone just perusing the files. But we do...

> Is there a reason for the renaming to all_topology Yes, coq gets confused having a folder and a file with the same name. It just won't build. Using `all_topology`...

Ok, just pushed a change with the folder renamed to `topology_theory` (seemed appropriate given the top level folder is `theories`). The export-everything file is now just `topology.v` as before. And...

On one hand, yes you might as well enjoy the improved generality of `realFieldType`. As to why it doesn't work, non-forgetful inheritance is easy to blame (although I admit I...

I agree, the way to_set worked was unsatisfactory. This at least consolidates the definition into one place, rather that redefining it. I'm happier with this (and I wouldn't use `xsect`,...

The problem I'm having is that it takes 3 minutes to run that one command. Since I know what structure i want it to saturate for, is there anyway for...

All the reshuffling of `topology_theory` seems to have unblocked this. Although the underlying issue is probably still around, this is now ready for a proper review

Makes sense to add this. I'll note that there are a handful of places (itll take me a minute to find them all) where we use pseudometric + hausdorff instead...