- Standardized prefix use of "Local"/"Global" modifiers as decided in

  late 2008 Coq WG.
- Updated Copyright file wrt JProver.



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

1 files changed, 8 insertions, 8 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 1294ee7c0b..502b42b837 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1150,15 +1150,15 @@ have to) be skipped in any expression involving an application of
 {\qualid}.
 
 \begin{Variants}
-\item {\tt Implicit Arguments Global {\qualid} [ \nelist{\possiblybracketedident}{} ]
-\comindex{Implicit Arguments Global}}
+\item {\tt Global Implicit Arguments {\qualid} [ \nelist{\possiblybracketedident}{} ]
+\comindex{Global Implicit Arguments}}
 
 Tells 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 Implicit Arguments Local {\qualid} [ \nelist{\possiblybracketedident}{} ]
-\comindex{Implicit Arguments Local}}
+\item {\tt Local Implicit Arguments {\qualid} [ \nelist{\possiblybracketedident}{} ]
+\comindex{Local Implicit Arguments}}
 
 When in a module, tells not to activate the implicit arguments of
 {\qualid} declared by this commands to contexts that requires the
@@ -1210,14 +1210,14 @@ Sections~\ref{SetStrictImplicit},~\ref{SetContextualImplicit},~\ref{SetReversibl
 and also~\ref{SetMaximalImplicitInsertion}).
 
 \begin{Variants}
-\item {\tt Implicit Arguments Global {\qualid}
-\comindex{Implicit Arguments Global}}
+\item {\tt Global Implicit Arguments {\qualid}
+\comindex{Global Implicit Arguments}}
 
 Tells to recompute the implicit arguments of {\qualid} after ending of
 the current section if any.
 
-\item {\tt Implicit Arguments Local {\qualid}
-\comindex{Implicit Arguments Local}}
+\item {\tt Local Implicit Arguments {\qualid}
+\comindex{Local Implicit Arguments}}
 
 When in a module, tells not to activate the implicit arguments of
 {\qualid} computed by this declaration to contexts that requires the