Remove workaround for bad documentation link in 8.3pl1, fixed in 8.3pl2.
Revert change in 8.3pl1-1 to split arch-specific stuff from noarch stuff.
Coq tactics are written in ocaml, which compiles to arch-specific files,
and those files are stored in the same place as the noarch proof files.