diff options
Diffstat (limited to 'doc/sphinx/proof-engine/ltac.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index d9a0178cce..e1f57c9bea 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -8,7 +8,7 @@ This chapter documents the tactic language |Ltac|. We start by giving the syntax followed by the informal semantics. To learn more about the language and especially about its foundations, please refer to :cite:`Del00`. -(Note the examples in the paper won't work as-is; |Coq| has evolved +(Note the examples in the paper won't work as-is; Coq has evolved since the paper was written.) .. example:: Basic tactic macros @@ -41,7 +41,7 @@ higher precedence than `+`. Usually `a/b/c` is given the :gdef:`left associativ interpretation `(a/b)/c` rather than the :gdef:`right associative` interpretation `a/(b/c)`. -In |Coq|, the expression :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; @tactic__4` +In Coq, the expression :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; @tactic__4` is interpreted as :n:`(try (repeat (@tactic__1 || @tactic__2)); @tactic__3); @tactic__4` because `||` is part of :token:`ltac_expr2`, which has higher precedence than :tacn:`try` and :tacn:`repeat` (at the level of :token:`ltac_expr3`), which @@ -784,7 +784,7 @@ single success: Checking for a single success: exactly_once ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -|Coq| provides an experimental way to check that a tactic has *exactly +Coq provides an experimental way to check that a tactic has *exactly one* success: .. tacn:: exactly_once @ltac_expr3 @@ -813,7 +813,7 @@ one* success: Checking for failure: assert_fails ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -|Coq| defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*: +Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*: .. tacn:: assert_fails @ltac_expr3 :name: assert_fails @@ -859,7 +859,7 @@ Checking for failure: assert_fails Checking for success: assert_succeeds ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -|Coq| defines an |Ltac| tactic in `Init.Tactics` to check that a tactic has *at least one* +Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic has *at least one* success: .. tacn:: assert_succeeds @ltac_expr3 @@ -905,7 +905,7 @@ Failing See the example for a comparison of the two constructs. - Note that if |Coq| terms have to be + Note that if Coq terms have to be printed as part of the failure, term construction always forces the tactic into the goals, meaning that if there are no goals when it is evaluated, a tactic call like :tacn:`let` :n:`x := H in` :tacn:`fail` `0 x` will succeed. @@ -990,7 +990,7 @@ amount of time: timeout with some other tacticals. This tactical is hence proposed only for convenience during debugging or other development phases, we strongly advise you to not leave any timeout in final scripts. Note also that - this tactical isn’t available on the native Windows port of |Coq|. + this tactical isn’t available on the native Windows port of Coq. Timing a tactic ~~~~~~~~~~~~~~~ @@ -1523,7 +1523,7 @@ produce subgoals but generates a term to be used in tactic expressions: Generating fresh hypothesis names ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Tactics sometimes need to generate new names for hypothesis. Letting |Coq| +Tactics sometimes need to generate new names for hypothesis. Letting Coq choose a name with the intro tactic is not so good since it is very awkward to retrieve that name. The following expression returns an identifier: @@ -1893,7 +1893,7 @@ Proving that a list is a permutation of a second list From Section :ref:`ltac-syntax` we know that Ltac has a primitive notion of integers, but they are only used as arguments for primitive tactics and we cannot make computations with them. Thus, - instead, we use |Coq|'s natural number type :g:`nat`. + instead, we use Coq's natural number type :g:`nat`. .. coqtop:: in |