Fixed a Not_found bug when declaring in a section some implicit

arguments for a constant not defined in the section.

Also fixed some typos in the doc of implicit arguments in the
reference manual.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14816 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 5 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 472d7903b8..2da5bec186 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1208,15 +1208,15 @@ have to) be skipped in any expression involving an application of
 \item {\tt Global Arguments {\qualid} \nelist{\possiblybracketedident}{}
 \comindex{Global Arguments}}
 
-Tells to recompute the implicit arguments of {\qualid} after ending of
+Tell to recompute the implicit arguments of {\qualid} after ending of
 the current section if any, enforcing the implicit arguments known
 from inside the section to be the ones declared by the command.
 
 \item {\tt Local Arguments {\qualid} \nelist{\possiblybracketedident}{}
 \comindex{Local Arguments}}
 
-When in a module, tells not to activate the implicit arguments of
-{\qualid} declared by this commands to contexts that requires the
+When in a module, tell not to activate the implicit arguments of
+{\qualid} declared by this command to contexts that require the
 module.
 
 \item {\tt \zeroone{Global {\sl |} Local} Arguments {\qualid} \sequence{\nelist{\possiblybracketedident}{}}{,}}
@@ -1283,13 +1283,13 @@ and also~\ref{SetMaximalImplicitInsertion}).
 \item {\tt Global Arguments {\qualid} : default implicits
 \comindex{Global Arguments}}
 
-Tells to recompute the implicit arguments of {\qualid} after ending of
+Tell to recompute the implicit arguments of {\qualid} after ending of
 the current section if any.
 
 \item {\tt Local Arguments {\qualid} : default implicits
 \comindex{Local Arguments}}
 
-When in a module, tells not to activate the implicit arguments of
+When in a module, tell not to activate the implicit arguments of
 {\qualid} computed by this declaration to contexts that requires the
 module.