Recursive [inv_vec].

3ebeaca2 · Jacques-Henri Jourdan · Robbert Krebbers · 0158faa7 · 3ebeaca2
Commit 3ebeaca2 authored Jan 06, 2017 by Jacques-Henri Jourdan Committed by Robbert Krebbers Jan 31, 2017
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 1 deletion

theories/vector.v theories/vector.v +2 -1

No files found.
--- 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