also ignore coq compiled .glob files
Case tactics from some wiki somewhere (they're not built in...)
Induction chapter up to "Proofs within proofs"