diff options
| author | Zeimer | 2018-08-04 16:29:06 +0200 |
|---|---|---|
| committer | Zeimer | 2018-08-31 09:45:17 +0200 |
| commit | a67fa614450467afbd56233f489b2105dc655a58 (patch) | |
| tree | 3050e3f03d09c79410f91b1a9a07b61baed7d38e /doc/sphinx/proof-engine/ltac.rst | |
| parent | bf1446294dba45d3ea9b7bb39d2fc96617848c03 (diff) | |
Uniformized many spelling variants. Added .. warning:: and .. seealso:: directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.
Diffstat (limited to 'doc/sphinx/proof-engine/ltac.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 0310dbead5..7608ea7245 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -556,9 +556,9 @@ Failing The number is the failure level. If no level is specified, it defaults to 0. The level is used by :tacn:`try`, :tacn:`repeat`, :tacn:`match goal` and the branching tacticals. If 0, it makes :tacn:`match goal` consider the next clause - (backtracking). If non zero, the current :tacn:`match goal` block, :tacn:`try`, + (backtracking). If nonzero, the current :tacn:`match goal` block, :tacn:`try`, :tacn:`repeat`, or branching command is aborted and the level is decremented. In - the case of :n:`+`, a non-zero level skips the first backtrack point, even if + the case of :n:`+`, a nonzero level skips the first backtrack point, even if the call to :n:`fail @num` is not enclosed in a :n:`+` command, respecting the algebraic identity. @@ -863,7 +863,7 @@ We can perform pattern matching on goals using the following expression: :name: match goal If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i = 1, ..., m\ :sub:`1` is - matched (non-linear first-order unification) by an hypothesis of the + matched (non-linear first-order unification) by a hypothesis of the goal and if :n:`cpattern_1` is matched by the conclusion of the goal, then :n:`@expr__1` is evaluated to :n:`v__1` by substituting the pattern matching to the metavariables and the real hypothesis names @@ -989,7 +989,7 @@ Manipulating untyped terms An untyped term, in |Ltac|, can contain references to hypotheses or to |Ltac| variables containing typed or untyped terms. An untyped term can be - type-checked using the function type_term whose argument is parsed as an + type checked using the function type_term whose argument is parsed as an untyped term and returns a well-typed term which can be used in tactics. Untyped terms built using :n:`uconstr :` can also be used as arguments to the |