When the user thinks he has completed his proof, he can save it by issuing the command Qed. At this point the proof object is built in its completeness, it is passed to the proof checker and the proof checker verifies the proof. If the proof is correct, it is saved together with the given name. At this point Coq switches back to normal mode and it is able to take more commands. Of course, saved proofs, that is saved terms, can be reused in other proofs, or may be saved in libraries, since in Coq there is no difference between primitive properties and properties obtained by means of proofs. And of course whole libraries can be restored by using the keyword Require.

---