Why is the crush tactic not found?

Using Coq
1

Going through a trivial exercise from Adam’s book but my proof general can’t find the tactic crush:

Error: The reference crush was not found in the current environment.

Why? And how do I put it in?

Module nn.
  Theorem add_induct2:
    forall n, n+0 = n.
  Proof.
    induction n; crush.
End nn.
2

That’s because crush is not a built in tactic. You should download the tarball for CPDT here, compile with make and work inside the folder.