diff options
| -rw-r--r-- | doc/refman/RefMan-lib.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-uti.tex | 6 | ||||
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 2 | ||||
| -rw-r--r-- | theories/Lists/List.v | 2 |
6 files changed, 10 insertions, 10 deletions
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex index 36549b7a0..31c6fef4a 100644 --- a/doc/refman/RefMan-lib.tex +++ b/doc/refman/RefMan-lib.tex @@ -997,7 +997,7 @@ Abort. \end{coq_eval} \item {\tt split\_Rabs} allows to unfold {\tt Rabs} constant and splits -corresponding conjonctions. +corresponding conjunctions. \tacindex{split\_Rabs} \begin{coq_example*} diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index f63a5044c..c524ecedd 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -861,7 +861,7 @@ declared or defined constant. We give an overview of the scopes used in the standard library of {\Coq}. For a complete list of notations in each scope, use the -commands {\tt Print Scopes} or {\tt Print Scopes {\scope}}. +commands {\tt Print Scopes} or {\tt Print Scope {\scope}}. \subsubsection{\tt type\_scope} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 09cce8788..5feafe740 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1289,8 +1289,8 @@ computational expressions (i.e. with few dead code). \item {\tt lazy [\qualid$_1$\ldots\qualid$_k$]}\\ {\tt lazy -[\qualid$_1$\ldots\qualid$_k$]} - These are respectively synonyms of {\tt cbv beta delta - [\qualid$_1$\ldots\qualid$_k$] iota zeta} and {\tt cbv beta delta + These are respectively synonyms of {\tt lazy beta delta + [\qualid$_1$\ldots\qualid$_k$] iota zeta} and {\tt lazy beta delta -[\qualid$_1$\ldots\qualid$_k$] iota zeta}. \item {\tt vm\_compute} \tacindex{vm\_compute} @@ -2684,7 +2684,7 @@ If {\term} is a proof of a statement of conclusion then {\tt injection} applies injectivity as deep as possible to derive the equality of all the subterms of {\term$_1$} and {\term$_2$} placed in the same positions. For example, from {\tt (S - (S n))=(S (S (S m))} we may derive {\tt n=(S m)}. To use this + (S n))=(S (S (S m)))} we may derive {\tt n=(S m)}. To use this tactic {\term$_1$} and {\term$_2$} should be elements of an inductive set and they should be neither explicitly equal, nor structurally different. We mean by this that, if {\tt n$_1$} and {\tt n$_2$} are diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 153532f0b..bda4cff9b 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -157,8 +157,8 @@ have been completely produced with {\tt coq-tex}. \subsection{The \Coq\ Emacs mode} \Coq\ comes with a Major mode for \emacs, {\tt coq.el}. This mode provides -syntax highlighting (assuming your \emacs\ library provides -{\tt hilit19.el}) and also a rudimentary indentation facility +syntax highlighting +and also a rudimentary indentation facility in the style of the Caml \emacs\ mode. Add the following lines to your \verb!.emacs! file: @@ -189,7 +189,7 @@ Instructions to use it are contained in this file. \subsection[Proof General]{Proof General\index{Proof General}} Proof General is a generic interface for proof assistants based on -Emacs (or XEmacs). The main idea is that the \Coq\ commands you are +Emacs. The main idea is that the \Coq\ commands you are editing are sent to a \Coq\ toplevel running behind Emacs and the answers of the system automatically inserted into other Emacs buffers. Thus you don't need to copy-paste the \Coq\ material from your files diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index b4e470470..f311d2447 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -1014,7 +1014,7 @@ Inductive h_step : Set := (* This type allows to navigate in the logical constructors that form the predicats of the hypothesis in order to decompose them. This allows in particular to extract one hypothesis from a - conjonction with possibly the right level of negations. *) + conjunction with possibly the right level of negations. *) Inductive direction : Set := | D_left : direction diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 84e145271..ecadddbc8 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -259,7 +259,7 @@ Section Facts. Qed. - (** Compatibility wtih other operations *) + (** Compatibility with other operations *) Lemma app_length : forall l l' : list A, length (l++l') = length l + length l'. Proof. |