From 4fffbe45f42517fbe41fbcf4bf77bfa72fff2579 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 19 Jan 2021 10:34:22 -0800
Subject: Remove convert_concl_no_check

---
 doc/sphinx/proofs/writing-proofs/rewriting.rst | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'doc/sphinx/proofs')

diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 8873d02888..5b9304102c 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
-- 
cgit v1.2.3