Stream: coq-community devs & users

Topic: Redundant file in coq-art repo

Karl Palmskog (Sep 23 2022 at 08:54):

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

Karl Palmskog (Sep 23 2022 at 09:18):

@Pierre Castéran we should remove sqrt_by_GhaS_See.v, right? The content is already in the other file, which is in _CoqProject.

Pierre Castéran (Sep 23 2022 at 09:40):

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: Jun 03 2023 at 18:01 UTC