affeldt-aist

@Tragicus had a look (including the changelog) so I might merge today to release.

This is different. I think that @gares is referring to printed material written mostly by @pi8027 that he has been distributing domestically. But I don't think you can find them...

Is this PR still under consideration?

master already has a `meta.yml` file that looks fine to apply the coq-community machinery, maybe this PR should be closed?

The CI error is: ```shell > COQC theories/lspace.v > File "./theories/lspace.v", line 82, characters 33-42: > Error: Syntax error: [reduce] expected after ':=' (in [def_body]). ```