Stream: Hierarchy Builder devs & users

Topic: HB_scope or hb_scope?

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

Enrico Tassi (Jun 20 2020 at 10:00):

Why the hb_scope in the CoqWS demo? @Cyril Cohen

Enrico Tassi (Jun 20 2020 at 10:42):

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

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?

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: Sep 15 2024 at 13:02 UTC