From 845e9b73230699686a121349c3a35d94c8e76e4c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 22 Jan 2017 12:46:13 +0100
Subject: [PATCH] Vector tweaks.

---
 theories/vector.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/vector.v b/theories/vector.v
index 5a7ed65c..84840dd7 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) =>
-- 
GitLab