diff options
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 02a0867341..bb7cac17b0 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4841,6 +4841,26 @@ Performance-oriented tactic variants exact I. Fail Qed. + :tacn:`change_no_check` supports all of `change`'s variants. + + .. tacv:: change_no_check @term with @term’ + :undocumented: + + .. tacv:: change_no_check @term at {+ @num} with @term’ + :undocumented: + + .. tacv:: change_no_check @term {? {? at {+ @num}} with @term} in @ident + + .. example:: + + .. coqtop:: all abort + + Goal True -> False. + intro H. + change_no_check False in H. + exact H. + Fail Qed. + .. tacv:: convert_concl_no_check @term :name: convert_concl_no_check |