diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 24 |
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*} |