diff options
| author | Paolo G. Giarrusso | 2019-05-03 01:13:48 +0200 |
|---|---|---|
| committer | Paolo G. Giarrusso | 2019-05-03 02:11:34 +0200 |
| commit | 590ee35546f3528ac7ccb32306fb86e78fdce93b (patch) | |
| tree | a8332f2c22f0b4e4450536e7b85ab08969d0bd1d | |
| parent | 70e01149ad4c74d086f042f0cced74b1d0e228bf (diff) | |
Documentation for change_no_check untested variants
Copy change's variants in change_no_check, since supposedly they should all be
supported. But they haven't been tested, and my example fails.
| -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 |