diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 8 | ||||
| -rw-r--r-- | doc/tools/Translator.tex | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 794804a1f6..26f4ec6242 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -103,7 +103,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms: .. exn:: Not the right number of missing arguments. -.. _occurencessets: +.. _occurrencessets: Occurrence sets and occurrence clauses ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1024,7 +1024,7 @@ Managing the local context This notation allows specifying which occurrences of :token:`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 <occurrencessets>`. .. tacv:: set (@ident @binders := @term) {? in @goal_occurrences } @@ -1509,7 +1509,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) This syntax is used for selecting which occurrences of :token:`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>`. + in :ref:`occurrences sets <occurrencessets>`. .. tacv:: destruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } edestruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } @@ -1659,7 +1659,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 <occurrencessets>`. 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. diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex index 3ee65d6f22..d8ac640f2a 100644 --- a/doc/tools/Translator.tex +++ b/doc/tools/Translator.tex @@ -490,7 +490,7 @@ to be applied are separated by a {\tt =>}. to turn implicit only the arguments that are {\em strictly} implicit (or rigid), i.e. that remains inferable whatever the other arguments are. For instance {\tt x} inferable from {\tt P x} is not strictly -inferable since it can disappears if {\tt P} is instanciated by a term +inferable since it can disappears if {\tt P} is instantiated by a term which erases {\tt x}. \begin{transbox} |