There was one more universe needed due to the use of now non-universe-polymorphic

ID, fixing the script results in 3 universes for the stdlib again.

1 files changed, 3 insertions, 3 deletions

diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index 3e8c1175f..7f4228dd6 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -62,12 +62,12 @@ Proof.
 refine (@Fin.rectS _ _ _); lazy beta; [ intros n v | intros n p H v ].
   revert n v; refine (@caseS _ _ _); simpl; intros. now destruct t.
   revert p H.
-  refine (match v as v' in t _ m return match m as m' return t A m' -> Type with
+  refine (match v as v' in t _ m return match m as m' return t A m' -> Prop with
     |S (S n) => fun v => forall p : Fin.t (S n),
       (forall v0 : t A (S n), (shiftrepeat v0) [@ Fin.L_R 1 p ] = v0 [@p]) ->
       (shiftrepeat v) [@Fin.L_R 1 (Fin.FS p)] = v [@Fin.FS p]
-    |_ => fun _ => @ID end v' with
-  |[] => @id |h :: t => _ end). destruct n0. exact @id. now simpl.
+    |_ => fun _ => True end v' with
+  |[] => I |h :: t => _ end). destruct n0. exact I. now simpl.
 Qed.
 
 Lemma shiftrepeat_last A: forall n (v: t A (S n)), last (shiftrepeat v) = last v.