5 files changed, 9 insertions, 15 deletions
diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex
index 0664bf9095..77d5928345 100644
--- a/doc/refman/Polynom.tex
+++ b/doc/refman/Polynom.tex
@@ -342,16 +342,16 @@ describes their syntax and effects:
   By default the tactic does not recognize power expressions as ring
   expressions.
 \item[sign {\term}] allows {\tt ring\_simplify} to use a minus operation
-  when outputing its normal form, i.e writing $x - y$ instead of $x + (-y)$. 
+  when outputting its normal form, i.e writing $x - y$ instead of $x + (-y)$.
   The term {\term} is a proof that a given sign function indicates expressions
    that are signed ({\term} has to be a
-  proof of {\tt Ring\_theory.get\_sign}). See  {\tt plugins/setoid\_ring/IntialRing.v} for examples of sign function.
-\item[div {\term}] allows  {\tt ring} and {\tt ring\_simplify} to use moniomals
+  proof of {\tt Ring\_theory.get\_sign}). See  {\tt plugins/setoid\_ring/InitialRing.v} for examples of sign function.
+\item[div {\term}] allows  {\tt ring} and {\tt ring\_simplify} to use monomials
 with coefficient other than 1 in the rewriting. The term {\term} is a proof that a given division function  satisfies the specification of an euclidean
   division function  ({\term} has to be a
   proof of {\tt Ring\_theory.div\_theory}). For example, this function is
   called when trying to rewrite $7x$ by $2x = z$ to tell that $7 = 3 * 2 + 1$.
-   See  {\tt plugins/setoid\_ring/IntialRing.v} for examples of div function.
+   See  {\tt plugins/setoid\_ring/InitialRing.v} for examples of div function.
   
 \end{description}
 
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index bef0a1686f..45230fb6e5 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -123,12 +123,6 @@ The following command-line options are recognized by the commands {\tt
   valid for {\tt coqc} as the toplevel module name is inferred from the
   name of the output file.
 
-\item[{\tt -notop}]\ %
-
-  Use the empty logical path for the toplevel module name instead of {\tt
-    Top}. Not valid for {\tt coqc} as the toplevel module name is
-  inferred from the name of the output file.
-
 \item[{\tt -exclude-dir} {\em directory}]\ %
 
   Exclude any subdirectory named {\em directory} while
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index b475a5233c..1d423f8b16 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -991,7 +991,7 @@ but library file names based on other roots can be obtained by using
 {\Coq} commands ({\tt coqc}, {\tt coqtop}, {\tt coqdep}, \dots) options
 {\tt -Q} or {\tt -R} (see Section~\ref{coqoptions}). Also, when an
 interactive {\Coq} session starts, a library of root {\tt Top} is
-started, unless option {\tt -top} or {\tt -notop} is set (see
+started, unless option {\tt -top} is set (see
 Section~\ref{coqoptions}).
 
 \subsection{Qualified names
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index c37367de5b..16c822b6a5 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -477,15 +477,15 @@ names.
 \item{\tt Show Intro.}\comindex{Show Intro}\\
 If the current goal begins by at least one product, this command
 prints the name of the first product, as it would be generated by 
-an anonymous {\tt Intro}. The aim of this command is to ease the
+an anonymous {\tt intro}. The aim of this command is to ease the
 writing of more robust scripts. For example, with an appropriate 
 {\ProofGeneral} macro, it is possible to transform any anonymous {\tt
-  Intro} into a qualified one such as {\tt Intro y13}.
+  intro} into a qualified one such as {\tt intro y13}.
 In the case of a non-product goal, it prints nothing. 
 
 \item{\tt Show Intros.}\comindex{Show Intros}\\
 This command is similar to the previous one, it simulates the naming 
-process of an {\tt Intros}.
+process of an {\tt intros}.
 
 \item{\tt Show Existentials.\label{ShowExistentials}}\comindex{Show Existentials}
 \\ It displays
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 61093709ec..ecaf82806e 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -120,7 +120,7 @@ Notation "A \/ B" := (or A B)  (at level 85, right associativity).
 
 By default, a notation is considered non associative, but the
 precedence level is mandatory (except for special cases whose level is
-canonical). The level is either a number or the mention {\tt next
+canonical). The level is either a number or the phrase {\tt next
 level} whose meaning is obvious. The list of levels already assigned
 is on Figure~\ref{init-notations}.