Stream: coq-community devs & users

Topic: Redundant file in coq-art repo


view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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: Feb 04 2023 at 02:03 UTC