add a command line option for turning off sharing

This gives better control than the old patch called
"fix-hanging-at-end-of-proof.patch".

The reason it's needed is that some proofs in Voevodsky's Foundations
hang forever at "Defined", and there seems to be no other way to
get coq to accept the proof.  Sharing is definitely useful for
some proofs, such as those in the standard coq library "Cyclic31",
so it's a good idea to have it under the control of the user.