Limitations of Qed on Let should be documented

[SkySkimmer]

Current doc:

coq/doc/sphinx/language/core/sections.rst

Lines 66 to 67 in 4db1523

	In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
	for which the computational behavior is relevant. See :ref:`proof-editing-mode`.

Limitations:

• Qed is not respected by the kernel inside the section (although it is respected by most tactics)
• Qed is fully equivalent to Defined after the section is closed

Demonstration:

Section S.
  Let x : nat. Proof. exact 0. Qed.

  Definition y := x.

  Lemma foo : y = 0.
  Proof.
    Fail reflexivity.
    exact_no_check (eq_refl 0).
  Qed.
End S.
Eval cbv in y. (* 0 *)

[Zimmi48]

Previous discussions on the topic:

• Let ... Qed. for vos #13584 (suggestion to emit a warning when using Qed after Let)
• Future of Let vernacular #10459

Also related:

• Coq should have more notions of Opacity #3389 (Coq should have more forms of opacity)