Commit 845e9b73 authored by Robbert Krebbers's avatar Robbert Krebbers

Vector tweaks.

parent eebf68aa
......@@ -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) =>
......
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