From 234f5479773d43a48e67c5c0ea361445c7fb6782 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sun, 22 Jul 2018 18:19:26 -0400 Subject: Correct some spelling errors Lintian found some spelling errors in the Debian packaging for coq. Fix them most places they appear in the current source. (Don't change documentation anchor names, as that would invalidate external deeplinks.) This also fixes a bug in coqdoc: prior to this commit, coqdoc would highlight `instanciate` but not `instantiate`. --- doc/sphinx/proof-engine/tactics.rst | 18 +++++++++--------- doc/tools/Translator.tex | 2 +- 2 files changed, 10 insertions(+), 10 deletions(-) (limited to 'doc') 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 `. + :ref:`goal occurrences `. .. 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 `. + :ref:`occurrences sets `. .. 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 `. If variables or hypotheses not + :ref:`occurrences sets `. 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 3ee65d6f2..d8ac640f2 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} -- cgit v1.2.3