Merge PR #13761: Remove convert_concl_no_check (deprecated in 8.11)

Reviewed-by: Zimmi48
Reviewed-by: ppedrot

3 files changed, 5 insertions, 8 deletions

diff --git a/doc/changelog/04-tactics/13761-remove_convert_concl_nc.rst b/doc/changelog/04-tactics/13761-remove_convert_concl_nc.rst
new file mode 100644
index 0000000000..1aa57ff8b1
--- /dev/null
+++ b/doc/changelog/04-tactics/13761-remove_convert_concl_nc.rst
@@ -0,0 +1,4 @@
+- **Removed:**
+  convert_concl_no_check.  Use :tacn:`change_no_check` instead
+  (`#13761 <https://github.com/coq/coq/pull/13761>`_,
+  by Jim Fehrle).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 7db54987d6..a08a110930 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -3191,7 +3191,7 @@ Other changes in 8.10+beta1
     by Maxime Dénès, review by Pierre-Marie Pédrot).
 
   - New variant :tacn:`change_no_check` of :tacn:`change`, usable as a
-    documented replacement of :tacn:`convert_concl_no_check`
+    documented replacement of `convert_concl_no_check`
     (`#10012 <https://github.com/coq/coq/pull/10012>`_,
     `#10017 <https://github.com/coq/coq/pull/10017>`_,
     `#10053 <https://github.com/coq/coq/pull/10053>`_, and
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 8c8c88c526..0a4a48555f 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -338,13 +338,6 @@ Rewriting with definitional equality
            exact H.
          Qed.
 
-   .. tacn:: convert_concl_no_check @one_term
-
-      .. deprecated:: 8.11
-
-      Deprecated old name for :tacn:`change_no_check`. Does not support any of its
-      variants.
-
 .. _performingcomputations:
 
 Performing computations