Commit 05b53000 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Recursive [inv_vec].

parent 66c3aff9
Pipeline #3620 passed with stage
in 10 minutes and 51 seconds
......@@ -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
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment