Add quick and vi2vo targets

It doesn't seem to help much at the moment, but maybe we'll grow some
very slow Qed'ed proofs and want to use this target.

c.f.
https://github.com/coq/coq/blob/trunk/doc/refman/AsyncProofs.tex#L98 for
documentation.

```bash
$ make clean
...
$ time make -j10
real    2m51.868s
user    4m7.179s
sys     8m45.765s

$ make clean
...
$ time make quick -j10

real    2m54.031s
user    4m15.360s
sys     8m52.969s

$ time make vi2vo J=10

real    0m21.458s
user    0m9.161s
sys     0m17.161s

```

This closes #471.