diff options
| author | Jim Fehrle | 2021-01-19 10:34:22 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2021-01-19 13:06:08 -0800 |
| commit | 4fffbe45f42517fbe41fbcf4bf77bfa72fff2579 (patch) | |
| tree | 15d1f73403e32d25322f43595eacc04fa12f26ea /doc/sphinx/proofs | |
| parent | f44e65e0d209fdada20998d661ad10a5e82a0d92 (diff) | |
Remove convert_concl_no_check
Diffstat (limited to 'doc/sphinx/proofs')
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 7 |
1 files changed, 0 insertions, 7 deletions
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 |