Remove everything after the content on goal management.

1 files changed, 0 insertions, 146 deletions

diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst
index fe9a31e220..1a8fd95892 100644
--- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst
+++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst
@@ -4829,149 +4829,3 @@ Non-logical tactics
 
    The ``give_up`` tactic can be used while editing a proof, to choose to
    write the proof script in a non-sequential order.
-
-Delaying solving unification constraints
-----------------------------------------
-
-.. tacn:: solve_constraints
-   :name: solve_constraints
-   :undocumented:
-
-.. flag:: Solve Unification Constraints
-
-   By default, after each tactic application, postponed typechecking unification
-   problems are resolved using heuristics. Unsetting this flag disables this
-   behavior, allowing tactics to leave unification constraints unsolved. Use the
-   :tacn:`solve_constraints` tactic at any point to solve the constraints.
-
-Proof maintenance
------------------
-
-*Experimental.*  Many tactics, such as :tacn:`intros`, can automatically generate names, such
-as "H0" or "H1" for a new hypothesis introduced from a goal.  Subsequent proof steps
-may explicitly refer to these names.  However, future versions of |Coq| may not assign
-names exactly the same way, which could cause the proof to fail because the
-new names don't match the explicit references in the proof.
-
-The following "Mangle Names" settings let users find all the
-places where proofs rely on automatically generated names, which can
-then be named explicitly to avoid any incompatibility.  These
-settings cause |Coq| to generate different names, producing errors for
-references to automatically generated names.
-
-.. flag:: Mangle Names
-
-   When set, generated names use the prefix specified in the following
-   option instead of the default prefix.
-
-.. opt:: Mangle Names Prefix @string
-   :name: Mangle Names Prefix
-
-   Specifies the prefix to use when generating names.
-
-Performance-oriented tactic variants
-------------------------------------
-
-.. tacn:: change_no_check @term
-   :name: change_no_check
-
-   For advanced usage. Similar to :tacn:`change` :n:`@term`, but as an optimization,
-   it skips checking that :n:`@term` is convertible to the goal.
-
-   Recall that the |Coq| kernel typechecks proofs again when they are concluded to
-   ensure safety. Hence, using :tacn:`change` checks convertibility twice
-   overall, while :tacn:`change_no_check` can produce ill-typed terms,
-   but checks convertibility only once.
-   Hence, :tacn:`change_no_check` can be useful to speed up certain proof
-   scripts, especially if one knows by construction that the argument is
-   indeed convertible to the goal.
-
-   In the following example, :tacn:`change_no_check` replaces :g:`False` by
-   :g:`True`, but :cmd:`Qed` then rejects the proof, ensuring consistency.
-
-   .. example::
-
-      .. coqtop:: all abort
-
-         Goal False.
-           change_no_check True.
-           exact I.
-         Fail Qed.
-
-   :tacn:`change_no_check` supports all of :tacn:`change`'s variants.
-
-   .. tacv:: change_no_check @term with @term’
-      :undocumented:
-
-   .. tacv:: change_no_check @term at {+ @natural} with @term’
-      :undocumented:
-
-   .. tacv:: change_no_check @term {? {? at {+ @natural}} with @term} in @ident
-
-      .. example::
-
-         .. coqtop:: all abort
-
-            Goal True -> False.
-              intro H.
-              change_no_check False in H.
-              exact H.
-            Fail Qed.
-
-   .. tacv:: convert_concl_no_check @term
-      :name: convert_concl_no_check
-
-      .. deprecated:: 8.11
-
-      Deprecated old name for :tacn:`change_no_check`. Does not support any of its
-      variants.
-
-.. tacn:: exact_no_check @term
-   :name: exact_no_check
-
-   For advanced usage. Similar to :tacn:`exact` :n:`@term`, but as an optimization,
-   it skips checking that :n:`@term` has the goal's type, relying on the kernel
-   check instead. See :tacn:`change_no_check` for more explanation.
-
-   .. example::
-
-      .. coqtop:: all abort
-
-         Goal False.
-           exact_no_check I.
-         Fail Qed.
-
-   .. tacv:: vm_cast_no_check @term
-      :name: vm_cast_no_check
-
-      For advanced usage. Similar to :tacn:`exact_no_check` :n:`@term`, but additionally
-      instructs the kernel to use :tacn:`vm_compute` to compare the
-      goal's type with the :n:`@term`'s type.
-
-      .. example::
-
-        .. coqtop:: all abort
-
-            Goal False.
-              vm_cast_no_check I.
-            Fail Qed.
-
-   .. tacv:: native_cast_no_check @term
-      :name: native_cast_no_check
-
-      for advanced usage. similar to :tacn:`exact_no_check` :n:`@term`, but additionally
-      instructs the kernel to use :tacn:`native_compute` to compare the goal's
-      type with the :n:`@term`'s type.
-
-      .. example::
-
-        .. coqtop:: all abort
-
-            Goal False.
-              native_cast_no_check I.
-            Fail Qed.
-
-.. [1] Actually, only the second subgoal will be generated since the
-  other one can be automatically checked.
-.. [2] This corresponds to the cut rule of sequent calculus.
-.. [3] Reminder: opaque constants will not be expanded by δ reductions.