I'd like to flag up that we now have these two files that seemingly have the same content in the coq-art repo:

- https://github.com/coq-community/coq-art/blob/master/ch15_general_recursion/SRC/sqrt_by_GhaS_See.v
- https://github.com/coq-community/coq-art/blob/master/ch15_general_recursion/SRC/sqrt_compute.v

@Pierre CastÃ©ran we should remove `sqrt_by_GhaS_See.v`

, right? The content is already in the other file, which is in `_CoqProject`

.

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 `Coq'Art`

?

Last updated: Feb 04 2023 at 02:03 UTC