Dan Christensen

And please keep your copy of the original repo that causes this. It sounds like you are able to reproduce the issue, which will be helpful in debugging it. Maybe...

That makes it really look like there is a bug in `borg compact`. @DSpammy , can you say more about how the repo was used? Was it always accessed locally?...

You can change the repo id in the config file in the borg repo you saved for testing. (Note that in general there are some risks if you do this...

The three segment files that gave errors were 48506 (twice), 47096, 26597. All three were *not* compacted during the `borg compact` run. Interesting...

I think it might be better to retain compatibility with the standard Coq library for this kind of thing (as much as possible). I often google things about nat in...

The search *results* are case sensitive! :-) But more important than the case is renaming things like `nat_add_comm` vs `nat_plus_comm`, so my comment is really more generally about trying to...

I asked Mike about this, and I was motivated by the fact that various mathematical software packages give advice about how to cite them, for example, [GAP](https://www.gap-system.org/Contacts/cite.html). I think it's...

It's unfortunate that so many proofs need a separate case now. I'd be interested to see whether this simplifies things in the Hurewicz branch, or means that additional cases need...

@Alizter If something like that works, it would be very nice. But the one thing I need doesn't seem to work. I have ```coq Definition AbHom' (A : Group) (B...

I'd still like to try my `GroupWithStructure` idea (or maybe it should be called `GroupWithProperty`), but I'm behind on too many things right now to give it a shot. If...