I'd like to flag up that we now have these two files that seemingly have the same content in the coq-art repo:
@Pierre Castéran we should remove
sqrt_by_GhaS_See.v, right? The content is already in the other file, which is in
OK for removing the old
sqrt_by_GhaS_See.v file (I just forgot to remove it once it was renamed). I'll do it now.
What about a simple public Zulip stream
Last updated: Feb 04 2023 at 02:03 UTC