This was asked by @Christian Doczkal and I don't know the answer.
It was introduced in the commit by @Cyril Cohen that made factory operations not suffixed with, say _f
, in a HB.builers
section, not sure it is related.
This is for backward compatibility reasons in case someone wrote explicitly e.g. Ring.add
I created a (minimal) example here. The Problem only shows up when importing the generated hierarchy: https://gist.github.com/chdoc/f50c3a15c41e92ec0ac89112f1e18fbe
The problem being that the reexport shadows the original notation for the relation/operation.
Indeed this is bad..., let's remove these reexports for now...
note that coq-elpi commands do understand attributes (eg #[verbose]
). We could have one attribute to enable MC specific backward compatibility code.
See also https://github.com/coq/coq/issues/10824
@Enrico Tassi that's what I meant in math-comp/hierarchy-builder#85 but I do not think it makes sense for the "reexport operations" bug
My point is that I don't know if we trigger a bug, see above, or if the code for backward compat is sometimes undesired.
I think the backward compatibility code is flawed anyway
(and that we might also trigger a bug)
Well, I'm of course biased, because I don't have HB code that's older than two days. But I would be happy if HB wouldn't trash my notations :sunglasses:
Last updated: May 28 2023 at 20:30 UTC