Make [path_induction] more robust

In newer trunks, it'll loop on section hypotheses.  See
https://coq.inria.fr/bugs/show_bug.cgi?id=3769.
Merge pull request #594 from JasonGross/robust-path-induction

Make [path_induction] more robust
add comment about updating to INSTALL.txt, close #501
Merge pull request #599 from mikeshulman/updating

add comment about updating to INSTALL.txt, close #501