Infoview variable grouping

Stream: general

[Yaël Dillies]

Imagine you have a bunch of objects of the same type in a proof or a bunch of similar hypotheses, but they aren't grouped in the infoview because they weren't introduced simultaneously. Is there/would it be possible to write a tactic that could untangle this mess at will? Or even better, is it possible to change the infoview so that it automatically groups terms of the same type together? I can't see a reason why you would want to keep them apart.

[Eric Wieser]

Dependent variables always appear after the variables they depend on in the current infoview

[Eric Wieser]

But otherwise you can revert then intro in a different order