aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx')
-rw-r--r--doc/sphinx/proof-engine/tactics.rst18
1 files changed, 9 insertions, 9 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 9b4d724e0..d1a685307 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -113,15 +113,15 @@ Occurrence sets and occurrence clauses
An occurrence clause is a modifier to some tactics that obeys the
following syntax:
-.. _tactic_occurence_grammar:
+.. _tactic_occurrence_grammar:
.. productionlist:: `sentence`
- occurence_clause : in `goal_occurences`
- goal_occurences : [ident [`at_occurences`], ... , ident [`at_occurences`] [|- [* [`at_occurences`]]]]
- :| * |- [* [`at_occurences`]]
- :| *
+ occurrence_clause : in `goal_occurrences`
+ goal_occurrences : [ident [`at_occurrences`], ... , ident [`at_occurrences`] [|- [* [`at_occurrences`]]]]
+ :| * |- [* [`at_occurrences`]]
+ :| *
at_occurrences : at `occurrences`
- occurences : [-] `num` ... `num`
+ occurrences : [-] `num` ... `num`
The role of an occurrence clause is to select a set of occurrences of a term in
a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate that
@@ -1002,7 +1002,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged.
This notation allows specifying which occurrences of :n:`@term` have to be
substituted in the context. The :n:`in @goal_occurrences` clause is an
occurrence clause whose syntax and behavior are described in
- :ref:`goal occurences <occurencessets>`.
+ :ref:`goal occurrences <occurencessets>`.
.. tacv:: set (@ident {+ @binder} := @term )
@@ -1483,7 +1483,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
This syntax is used for selecting which occurrences of :n:`@term` the case
analysis has to be done on. The :n:`in @goal_occurrences` clause is an
occurrence clause whose syntax and behavior is described in
- :ref:`occurences sets <occurencessets>`.
+ :ref:`occurrences sets <occurencessets>`.
.. tacv:: destruct @term with @bindings_list as @disj_conj_intro_pattern eqn:@naming_intro_pattern using @term with @bindings_list in @goal_occurrences
.. tacv:: edestruct @term with @bindings_list as @disj_conj_intro_pattern eqn:@naming_intro_pattern using @term with @bindings_list in @goal_occurrences
@@ -1631,7 +1631,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
This syntax is used for selecting which occurrences of :n:`@term` the
induction has to be carried on. The :n:`in @goal_occurrences` clause is an
occurrence clause whose syntax and behavior is described in
- :ref:`occurences sets <occurencessets>`. If variables or hypotheses not
+ :ref:`occurrences sets <occurencessets>`. If variables or hypotheses not
mentioning :n:`@term` in their type are listed in :n:`@goal_occurrences`,
those are generalized as well in the statement to prove.