Merge branch 'require-vector' into 'master'

Explicitly Require Coq Vector in vector.v (for coq/coq#18936)

See merge request !550

stdpp/vector.v

@@ -2,6 +2,11 @@
 (lists of fixed length). It uses the definitions from the standard library, but
 renames or changes their notations, so that it becomes more consistent with the
 naming conventions in this development. *)
+(* Coq warns about using vector, but it is not deprecated. Instead somehow they seem concerned
+about people having too much fun with type indices. See
+<https://github.com/coq/coq/pull/18032> for discussion. Let's just silence that. *)
+Local Set Warnings "-stdlib-vector".
+From Coq Require Vector.
 From stdpp Require Import countable.
 From stdpp Require Export fin list.
 From stdpp Require Import options.