diff options
Diffstat (limited to 'doc/sphinx/proof-engine/ltac.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index f18569c7fd..37d12e8ce5 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 @@ Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *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 @@ -904,7 +904,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. @@ -989,7 +989,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 ~~~~~~~~~~~~~~~ @@ -1884,7 +1884,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 |