Vector bundles

Stream: PR reviews

[Patrick Massot]

I tried to have a look at #14462 and #14484 but they are pretty difficult to assess without seeing how it works for all the intended construction, including hom bundles. I'm tempted to simply merge them and wait for the new hom bundle PR. But I'd like to make sure @Sebastien Gouezel doesn't want to say something first and then clarify the conflicting status. @Floris van Doorn can we now merge those two PRs at once or is there still a preferred order?

[Floris van Doorn]

No strong preference, but #14462 first might be a bit nicer.