diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 15 |
2 files changed, 16 insertions, 5 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 79eddbd3b5..6efc634087 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -516,7 +516,9 @@ Coq provides a derived tactic to check that a tactic *fails*: .. tacn:: assert_fails @ltac_expr :name: assert_fails - This behaves like :n:`tryif @ltac_expr then fail 0 tac "succeeds" else idtac`. + This behaves like :tacn:`idtac` if :n:`@ltac_expr` fails, and + behaves like :n:`fail 0 @ltac_expr "succeeds"` if :n:`@ltac_expr` + has at least one success. Checking the success ~~~~~~~~~~~~~~~~~~~~ @@ -528,7 +530,7 @@ success: :name: assert_succeeds This behaves like - :n:`tryif (assert_fails tac) then fail 0 tac "fails" else idtac`. + :n:`tryif (assert_fails @ltac_expr) then fail 0 @ltac_expr "fails" else idtac`. Solving ~~~~~~~ diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 57a54bc0ad..00f8269dc3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -535,7 +535,7 @@ Requesting information eexists ?[n]. Show n. - .. cmdv:: Show Proof + .. cmdv:: Show Proof {? Diffs {? removed } } :name: Show Proof Displays the proof term generated by the tactics @@ -544,6 +544,12 @@ Requesting information constructed. Each hole is an existential variable, which appears as a question mark followed by an identifier. + Experimental: Specifying “Diffs” highlights the difference between the + current and previous proof step. By default, the command shows the + output once with additions highlighted. Including “removed” shows + the output twice: once showing removals and once showing additions. + It does not examine the :opt:`Diffs` option. See :ref:`showing_diffs`. + .. cmdv:: Show Conjectures :name: Show Conjectures @@ -624,8 +630,11 @@ Showing differences between proof steps --------------------------------------- -Coq can automatically highlight the differences between successive proof steps and between -values in some error messages. +Coq can automatically highlight the differences between successive proof steps +and between values in some error messages. Also, as an experimental feature, +Coq can also highlight differences between proof steps shown in the :cmd:`Show Proof` +command, but only, for now, when using coqtop and Proof General. + For example, the following screenshots of CoqIDE and coqtop show the application of the same :tacn:`intros` tactic. The tactic creates two new hypotheses, highlighted in green. The conclusion is entirely in pale green because although it’s changed, no tokens were added |