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/changelog/04-tactics/13761-remove_convert_concl_nc.rst | 4 ++++ doc/sphinx/changes.rst | 2 +- doc/sphinx/proofs/writing-proofs/rewriting.rst | 7 ------- 3 files changed, 5 insertions(+), 8 deletions(-) create mode 100644 doc/changelog/04-tactics/13761-remove_convert_concl_nc.rst (limited to 'doc') 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 `_, + 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 `_, `#10017 `_, `#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 -- cgit v1.2.3