Rewrite Vector using list and small inversions

[andres-erbsen]

Closes #54

This PR is WIP but illustrative enough to see the direction. The idea is to keep the same type but remove anything that looks archaic, aiming for easy portability from old vector rather than drop-in compatibility.

Compat strategy:

• First release: Vector and Fin wrap Compat.Vector92 and Compat.Fin92 when compatible, incompatible interfaces are deprecated.
• Second release: Vector and Fin are replaced with new files, Compat.Vector92 and Compat.Fin92 do Require Export.

WIP steps:

• Do we want to rename the modules and types? (see below)
• Should new Vector stay template polymorphic? (this would be unfortunate but may be necessary for compat)
• Transitional wrapper defining current vector in terms of new vector
• Last remaining (boring) proof wrappers
• Added changelog.
• Added / updated documentation.
• Opened overlay pull requests.
  • elpi tests that rely on kernel path to Vector.t

The main consideration for potential renaming is that the following ought to be able to coexist (and be distinguishable):

• (current) Vector
• Fixpoint of pairs isomorphic to current vector
• sig list isomorphic to current vector
• heterogeneous vector (Inductive indexed by list of type)
• heterogeneous vector (Fixpoint consuming list of type returning pairs
• heterogeneous vector (Fixpoint consuming list of type returning primitive pairs
• Vector of sigT, constrained to have the right types using sig (maybe this one is silly)
• list of sigT constrained to have the right length and types