Laurent Théry (Apr 01 2021 at 14:32): Laurent Théry (Apr 01 2021 at 14:32):Hi, I am doing my night classes. Where can I find the flags that exists like verbose and mathcomp and what they are doing?
Enrico Tassi (Apr 01 2021 at 14:34):The best "doc" is here: https://github.com/math-comp/hierarchy-builder/blob/master/structures.v#L331
Enrico Tassi (Apr 01 2021 at 14:34):@Cyril Cohen I don't have the button to make a thread out of these 2 messages, please use your suporpowers
Laurent Théry (Apr 01 2021 at 14:43):So in [#mathcomp] the notations [myStructureType of ...] is not generated?
Cyril Cohen (Apr 01 2021 at 14:45):No, our dear coq-elpi maintainer did not bind string notations yet...
Last updated: May 28 2023 at 18:29 UTC