From 3ebeaca26a7c7e64a1113f0157f380cdfe857a77 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 6 Jan 2017 14:11:46 +0100
Subject: [PATCH] Recursive [inv_vec].

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

diff --git a/theories/vector.v b/theories/vector.v
index ef6d2d4b..5a7ed65c 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -191,7 +191,8 @@ Ltac inv_vec v :=
   | 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
+    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)
   end.
 
 (** The following tactic performs case analysis on all hypotheses of the shape
-- 
GitLab