I have entered the following code in CoqIde:
Require Export Classical.
Require Export Description.
Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}.
Theorem classical_definite_description :
forall (A : Type) (P : A->Prop), inhabited A ->
{ x : A | (exists! x : A, P x) -> P x }.
The message Nested proofs are not allowed unless you turn option Nested Proofs Allowed on.
is produced. How can I turn on the option Nested Proofs Allowed?