This Coq-club thread contains an interesting discussion about how to stay oriented while doing large inductive proofs.

Benjamin Pierce suggests using a Case tactic to mark your progress.

Since Coq version 8.2, the best way of organizing a large proof is probably using C-zar, Coq's DeclarativeProof language [http://www.lix.polytechnique.fr/coq/distrib/current/refman/Reference-Manual014.html]. You can use `escape` and `return` commands to include a procedural block in a declarative script, or `proof` and `end proof` to nest a declarative proof block inside a procedural proof script.