diff --git a/theories/vector.v b/theories/vector.v
index 5a7ed65c1fe35fc614d881c27c437dfd0d032449..84840dd7e0679e5433dee9d5c1affa6a6b3b09ff 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -187,7 +187,8 @@ Proof.
 Defined.
 
 Ltac inv_vec v :=
-  match type of v with
+  let T := type of v in
+  match eval hnf in T with
   | vec _ 0 =>
     revert dependent v; match goal with |- ∀ v, @?P v => apply (vec_0_inv P) end
   | vec _ (S ?n) =>