Stream: Hierarchy Builder devs & users

Topic: HB_scope or hb_scope?


view this post on Zulip Enrico Tassi (Jun 20 2020 at 10:00):

Here https://github.com/math-comp/hierarchy-builder/blob/8366979b187fb8a52a425f8a55bf466b85999708/Coq2020_material/example.v#L5
and here https://github.com/math-comp/hierarchy-builder/blob/8366979b187fb8a52a425f8a55bf466b85999708/structures.v#L20

view this post on Zulip Enrico Tassi (Jun 20 2020 at 10:00):

Why the hb_scope in the CoqWS demo? @Cyril Cohen

view this post on Zulip Enrico Tassi (Jun 20 2020 at 10:42):

Oh wait, it was not CohenCyril, but cyrilcohen who did the commit. We have been hacked ;-)

view this post on Zulip Cyril Cohen (Jun 20 2020 at 19:06):

Enrico Tassi said:

Oh wait, it was not CohenCyril, but cyrilcohen who did the commit. We have been hacked ;-)

Wtf?

view this post on Zulip Cyril Cohen (Jun 20 2020 at 19:14):

Enrico Tassi said:

Here https://github.com/math-comp/hierarchy-builder/blob/8366979b187fb8a52a425f8a55bf466b85999708/Coq2020_material/example.v#L5
and here https://github.com/math-comp/hierarchy-builder/blob/8366979b187fb8a52a425f8a55bf466b85999708/structures.v#L20

Yep, that's a superfluous copy-paste


Last updated: Jan 29 2023 at 16:02 UTC