[feature] Support minimizing multiple files simultaneously without merging them

[JasonGross]

Sometimes there may not be a way to merge files, so, as suggested by @SkySkimmer at coq/coq#14541 (comment), it would be nice to support simultaneously minimizing multiple files.

---

Indeed, global side effects of Require cause issues with the minimizer, and I may eventually have the minimizer handle multiple files to deal with this. But handling multiple files is an enormous increase in complexity. At a minimum, I'd have to handle the following:

• having two copies of the dependent file, one for producing the .vo associated with the coqc that should succeed, and another for the coqc that should fail
• somehow convincing coqc to load my version of the file rather than the one from the original development, ideally without breaking the contract that the minimizer doesn't change .v files in your development. Note that the original development still needs to be bound for the other Requires to work. I suppose I could copy the entire development tree to a new location, and operate on that in place, but this is still moderately more complex (and fails pretty badly if the minimizer is also trying to inline things from user-contrib, which it generally is).

If it's not too complicated to add an attribute that allows setting the unshadowable absolute name, I'd very much appreciate that.

Originally posted by @JasonGross in coq/coq#14541 (comment)

---

Note also that copying the whole development tree including .vo files may be expensive space-wise, and AFAIK there's no easy way to discover what OCaml compiler outputs I have to copy and where I have to put them to get OCaml plugins to work (let alone copying other dependencies like elpi files), which suggests that in fact I'd end up having to copy everything in the search path of coqc.

Originally posted by @JasonGross in coq/coq#14541 (comment)

---

Probably the way to do this is to allow a sort of meta-level format of multiple Coq files in the same minimized file, and stick them somewhere where they'll be preferentially picked up when compiling.