6 files changed, 5 insertions, 30 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 d9e4e4f2b3..38c1424379 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 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
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 069a342b2a..82b41e41bd 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -11,7 +11,6 @@
 {
 
 open Pp
-open Constr
 open Stdarg
 open Pcoq.Prim
 open Pcoq.Constr
@@ -199,20 +198,6 @@ TACTIC EXTEND unify
 END
 
 {
-let deprecated_convert_concl_no_check =
-  CWarnings.create
-    ~name:"convert_concl_no_check" ~category:"deprecated"
-    (fun () -> Pp.str "The syntax [convert_concl_no_check] is deprecated. Use [change_no_check] instead.")
-}
-
-TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> {
-    deprecated_convert_concl_no_check ();
-    Tactics.convert_concl ~check:false x DEFAULTcast
-  }
-END
-
-{
 
 let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid
 let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b40bdbc25e..3c51b0fe40 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -156,9 +156,6 @@ let convert_hyp ~check ~reorder d =
     end
   end
 
-let convert_concl_no_check = convert_concl ~check:false
-let convert_hyp_no_check = convert_hyp ~check:false ~reorder:false
-
 let convert_gen pb x y =
   Proofview.Goal.enter begin fun gl ->
     match Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y with
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index a6471be549..d93f3bc434 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -35,10 +35,6 @@ val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool
 val introduction    : Id.t -> unit Proofview.tactic
 val convert_concl   : check:bool -> types -> cast_kind -> unit Proofview.tactic
 val convert_hyp     : check:bool -> reorder:bool -> named_declaration -> unit Proofview.tactic
-val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
-[@@ocaml.deprecated "use [Tactics.convert_concl]"]
-val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
-[@@ocaml.deprecated "use [Tactics.convert_hyp]"]
 val mutual_fix      :
   Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic
 val fix             : Id.t -> int -> unit Proofview.tactic