Ralph Matthes

Concerning `CONTENTS.md`, this is sometimes irritating enough that it has to be committed so often. Having dozens of such files does not look good for me.

I looked into the [YAML file](https://github.com/UniMath/UniMath/blob/master/.github/workflows/build-libs.yml). It does not mention GrpdHIT in the step description (trivial to add). Why are the satellites not compiled with `make -j2`? Way over 3h...

Concerning the warnings I mentioned three days ago: compiling `GrpdHITs` according to the instructions produces an enormous number of warnings of the same type that can be suppressed with the...

In my experience, the hyperthreading of ordinary consumer Intel and AMD processors does not bring any gain in compilation time (but is likely to consume more RAM). Hence, the number...

I work on desktop computers at home and in the university since they compile UniMath quicker than affordable laptops. When moving between the two locations, I more and more often...

I find this proposal very interesting. A look into the recent history of Coq in the reference manual reveals that this feature has been available since version 8.9. Should it...

I made a small try in PR #1580 for SubstitutionSystems (the package) and in PR #1581 for bicategories (all files that import the file with their definition). These two parts...

So, in rounded figures, 300 out of the 770 .v files are already "under control". And future files that import any of those will be as well.

A new try is now in PR #1582 . Tested with the package PAdics that I had rewritten some years ago to conform mostly (as shown by the needed changes...

The line that turns our specific checks off is seen [here](https://github.com/rmatthes/UniMath/blob/issue1576forbifunctors/UniMath/CategoryTheory/Monoidal/DisplayedCartesianMonoidalCategoriesWhiskered.v#L280). The line Niels was referring to shows how to switch back to our style enforcement. Most of the code...