No section discharge for alias factories and builder mixins

[CohenCyril]

This is not a fix for #182. But it still makes sense

[gares]

Attributes are only looked up in the hypothetical context, not the whole program. Your intuition is nice, but I don't think I can implement it :-/

[CohenCyril]

Attributes are only looked up in the hypothetical context, not the whole program. Your intuition is nice, but I don't think I can implement it :-/

It's ok I invented a new clause dedicated to that... My main problem is understanding how to work around rocq-prover/rocq#13903, but «c'est casse-gueule».

[gares]

Something is fishy, vars should be closed wrt their type.

[gares]

You could use the code I wrote to discharge by hand record factories, a part of it actually...

[CohenCyril]

You could use the code I wrote to discharge by hand record factories, a part of it actually...

Actually, your trick for factories relied on the fact that the factory was not used in the section it was defined in. So that you can close the section and rebuild the record after that. However we cannot do this for builder instances because they are gradually used in the same section.
Moreover for factories the section environement was totally under our control, but in a builders section the user may add a new Variable for some reason and we do not want to use those. Rather than writing an additional mechanism to detect these user interference and warn/error, I think it would be better to close the using transitively, and use @using! _ =>.

[gares]

I can maybe fix @using! In coq Elpi waiting for the fix in coq proper... But next week :-)

[CohenCyril]

@gares @proux01 I opened an issue #182 with a minimized counterexample for the time being.

[gares]

What should we do with this PR? The coq issue is closed (in 8.14) and HB.instance K V deprecated.

[gares]

@CohenCyril it may be nice to have a test for this feature in the test suite, can you add it?