aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/proof-engine/proof-handling.rst
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-04-24 11:59:49 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-05-05 11:54:02 +0200
commit21c7793a458848e941a0a6edeb216c2076d947e5 (patch)
tree9fad9402e63c626fcb142514845cba05e0c4477f /doc/sphinx/proof-engine/proof-handling.rst
parent1ccb800d20f91f1566d59b549a8422f2230c25d5 (diff)
[sphinx] Fix some references.
Diffstat (limited to 'doc/sphinx/proof-engine/proof-handling.rst')
-rw-r--r--doc/sphinx/proof-engine/proof-handling.rst15
1 files changed, 7 insertions, 8 deletions
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index f62e95669..64e28cea4 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -542,13 +542,13 @@ debugging universe inconsistencies.
.. cmd:: Guarded.
-Some tactics (e.g. :tacn:`refine` :ref:`applyingtheorems`) allow to build proofs using
+Some tactics (e.g. :tacn:`refine`) allow to build proofs using
fixpoint or co-fixpoint constructions. Due to the incremental nature
of interactive proof construction, the check of the termination (or
guardedness) of the recursive calls in the fixpoint or cofixpoint
constructions is postponed to the time of the completion of the proof.
-The command ``Guarded`` allows checking if the guard condition for
+The command :cmd:`Guarded` allows checking if the guard condition for
fixpoint and cofixpoint is violated at some time of the construction
of the proof without having to wait the completion of the proof.
@@ -570,13 +570,12 @@ available hypotheses.
This option controls the way binders are handled
in assertion commands such as ``Theorem ident [binders] : form``. When the
-option is set, which is the default, binders are automatically put in
+option is on, which is the default, binders are automatically put in
the local context of the goal to prove.
-The option can be unset by issuing ``Unset Automatic Introduction``. When
-the option is unset, binders are discharged on the statement to be
-proved and a tactic such as intro (see Section :ref:`managingthelocalcontext`) has to be
-used to move the assumptions to the local context.
+When the option is off, binders are discharged on the statement to be
+proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`)
+has to be used to move the assumptions to the local context.
Controlling memory usage
@@ -597,4 +596,4 @@ the ongoing proof.
This command forces the |OCaml| runtime to perform a heap compaction.
This is in general an expensive operation.
See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
-There is also an analogous tactic :tac:`optimize_heap`.
+There is also an analogous tactic :tacn:`optimize_heap`.