Restored old behavior of injection on proofs by default.

Use Set Injection On Proof to enable the new behavior.
Suggest Set Injection On Proofs in error message for injection.
When discrimination is not possible, try to project.

Example:
Inductive Pnat : Prop := O | S : Pnat -> Pnat.

Variable m n : Pnat.

Goal S (S O) = S O -> False.
intros H; injection H.

now deduces S O = O instead of failing with an error message.