From 1de37fd615d39f11227c9ab6e792c707bfcafbe6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 15 Mar 2017 14:13:33 +0100
Subject: [PATCH] improve inv_vec to force the length of the vector

---
 theories/vector.v | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/theories/vector.v b/theories/vector.v
index 13ed7220..9d5b583d 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -189,11 +189,14 @@ Defined.
 Ltac inv_vec v :=
   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) =>
-    revert dependent v; match goal with |- ∀ v, @?P v => apply (vec_S_inv P) end;
-    try (let x := fresh "x" in intros x v; inv_vec v; revert x)
+  | vec _ ?n =>
+    match eval hnf in n with
+    | 0 => revert dependent v; match goal with |- ∀ v, @?P v => apply (vec_0_inv P) end
+    | S ?n =>
+      revert dependent v; match goal with |- ∀ v, @?P v => apply (vec_S_inv P) end;
+      (* Try going on recursively. *)
+      try (let x := fresh "x" in intros x v; inv_vec v; revert x)
+    end
   end.
 
 (** The following tactic performs case analysis on all hypotheses of the shape
-- 
GitLab