aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-02-10 13:24:55 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-02-10 13:24:55 +0100
commit804421f10f474d458a9bb8d62c67b97216f77aae (patch)
tree8ed42ba160c60ace08d77d51fa77563869285556 /doc
parentbcc050beebe32a1d94844875cf1e8c752e4b3985 (diff)
Fix some documentation typo.
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/RefMan-tac.tex24
1 files changed, 12 insertions, 12 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index dcc2bcc1f..33f6730e0 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -906,7 +906,7 @@ containing {\tt *} or {\tt **}, {\tt intros $p_1$ ... $p_n$}
variables or hypotheses until the goal is not any more a
quantification or an implication;
\item introduction over an introduction pattern $p$ introduces the
- forthcoming quantified variables or premisse of the goal and applies
+ forthcoming quantified variables or premise of the goal and applies
the introduction pattern $p$ to it.
\end{itemize}
@@ -1020,13 +1020,13 @@ dependencies. This tactic is the inverse of {\tt intro}.
This moves the hypothesis named {\ident$_1$} in the local context
after the hypothesis named {\ident$_2$}. The proof term is not changed.
-If {\ident$_1$} comes before {\ident$_2$} in the order of dependences,
-then all hypotheses between {\ident$_1$} and {\ident$_2$} that
-(possibly indirectly) depend on {\ident$_1$} are moved also.
+If {\ident$_1$} comes before {\ident$_2$} in the order of dependencies,
+then all the hypotheses between {\ident$_1$} and {\ident$_2$} that
+(possibly indirectly) depend on {\ident$_1$} are moved too.
-If {\ident$_1$} comes after {\ident$_2$} in the order of dependences,
-then all hypotheses between {\ident$_1$} and {\ident$_2$} that
-(possibly indirectly) occur in {\ident$_1$} are moved also.
+If {\ident$_1$} comes after {\ident$_2$} in the order of dependencies,
+then all the hypotheses between {\ident$_1$} and {\ident$_2$} that
+(possibly indirectly) occur in {\ident$_1$} are moved too.
\begin{Variants}
@@ -1415,7 +1415,7 @@ the number of the existential variable since this number is different
in every session.
When you are referring to hypotheses which you did not name
-explicitely, be aware that Coq may make a different decision on how to
+explicitly, be aware that Coq may make a different decision on how to
name the variable in the current goal and in the context of the
existential variable. This can lead to surprising behaviors.
@@ -1445,7 +1445,7 @@ a hypothesis or in the body or the type of a local definition.
\label{admit}
The {\tt admit} tactic ``solves'' the current subgoal by an
-axiom. This typically allows temporarily skiping a subgoal so as to
+axiom. This typically allows temporarily skipping a subgoal so as to
progress further in the rest of the proof. To know if some proof still
relies on unproved subgoals, one can use the command {\tt Print
Assumptions} (see Section~\ref{PrintAssumptions}). Admitted subgoals
@@ -2744,7 +2744,7 @@ the same variants as {\tt rewrite} has.
This tactic applies to any goal. It replaces all free occurrences of
{\term$_1$} in the current goal with {\term$_2$} and generates the
equality {\term$_2$}{\tt =}{\term$_1$} as a subgoal. This equality is
-automatically solved if it occurs amongst the assumption, or if its
+automatically solved if it occurs among the assumption, or if its
symmetric form occurs. It is equivalent to {\tt cut
\term$_2$=\term$_1$; [intro H{\sl n}; rewrite <- H{\sl n}; clear H{\sl
n}| assumption || symmetry; try assumption]}.
@@ -3034,7 +3034,7 @@ computational expressions (i.e. with few dead code).
\cite{CompiledStrongReduction}. This algorithm is dramatically more efficient
than the algorithm used for the {\tt cbv} tactic, but it cannot be
fine-tuned. It is specially interesting for full evaluation of algebraic
- objects. This includes the case of reflexion-based tactics.
+ objects. This includes the case of reflection-based tactics.
\item {\tt native\_compute} \tacindex{native\_compute}
@@ -4781,7 +4781,7 @@ Reset Initial.
This tactic puts the {\num} first goals at the end of the list of
goals. If {\num} is negative, it will put the last $\left|\num\right|$ goals at
-the begining of the list.
+the beginning of the list.
\Example
\begin{coq_example*}