- 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

4 files changed, 24 insertions, 23 deletions

diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex
index b4bae4235..6877db179 100644
--- a/doc/refman/Coercion.tex
+++ b/doc/refman/Coercion.tex
@@ -181,8 +181,8 @@ valid coercion paths are ignored; they are signaled by a warning.
 \end{enumerate}
 
 \begin{Variants}
-\item {\tt Coercion Local {\qualid} : {\class$_1$} >-> {\class$_2$}.}
-\comindex{Coercion Local}\\
+\item {\tt Local Coercion {\qualid} : {\class$_1$} >-> {\class$_2$}.}
+\comindex{Local Coercion}\\
   Declares the construction denoted by {\qualid} as a coercion local to
   the current section.
 
@@ -196,8 +196,8 @@ valid coercion paths are ignored; they are signaled by a warning.
   \texttt{Definition {\ident} : {\type} := {\term}}, and then
   declares {\ident} as a coercion between it source and its target. 
 
-\item {\tt Coercion Local {\ident} := {\term}}\comindex{Coercion Local}\\
-  This defines {\ident} just like \texttt{Local {\ident} :=
+\item {\tt Local Coercion {\ident} := {\term}}\comindex{Local Coercion}\\
+  This defines {\ident} just like \texttt{Let {\ident} :=
     {\term}}, and then declares {\ident} as a coercion between it
   source and its target.
 
@@ -263,7 +263,7 @@ coercion between {\class$_1$} and {\class$_2$}.
 \end{ErrMsgs}
 
 \begin{Variants}
-\item {\tt Identity Coercion Local {\ident}:{\ident$_1$} >-> {\ident$_2$}.} \\
+\item {\tt Local Identity Coercion {\ident}:{\ident$_1$} >-> {\ident$_2$}.} \\
 Idem but locally to the current section.
 
 \item {\tt SubClass {\ident} := {\type}.} \\
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 1294ee7c0..502b42b83 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
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 967a8180a..6ade546b0 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -445,13 +445,13 @@ Locate "'exists' _ , _".
 \begin{centerframe}
 \begin{tabular}{lcl}
 {\sentence} & ::= & 
-   \texttt{Notation} \zeroone{\tt Local} {\str} \texttt{:=} {\term} 
+   \zeroone{\tt Local} \texttt{Notation} {\str} \texttt{:=} {\term} 
    \zeroone{\modifiers} \zeroone{:{\scope}} .\\
   & $|$ & 
-   \texttt{Infix} \zeroone{\tt Local} {\str} \texttt{:=} {\qualid} 
+   \zeroone{\tt Local} \texttt{Infix} {\str} \texttt{:=} {\qualid} 
    \zeroone{\modifiers} \zeroone{:{\scope}} .\\
   & $|$ & 
-   \texttt{Reserved Notation} \zeroone{\tt Local} {\str}
+   \zeroone{\tt Local} \texttt{Reserved Notation} {\str}
    \zeroone{\modifiers} .\\
   & $|$ & {\tt Inductive}
    \nelist{{\inductivebody} \zeroone{\declnotation}}{with}{\tt .}\\
@@ -625,7 +625,7 @@ the underlying \verb="{ x }"=-free rule which is \verb="y & z"=).
 \paragraph{Persistence of notations}
 
 Notations do not survive the end of sections. They survive modules
-unless the command {\tt Notation Local} is used instead of {\tt
+unless the command {\tt Local Notation} is used instead of {\tt
 Notation}.
 
 \section[Interpretation scopes]{Interpretation scopes\index{Interpretation scopes}
@@ -693,9 +693,9 @@ exported to the modules that import the module where they occur.
 
 \begin{Variants}
 
-\item {\tt Open Local Scope} {\scope}.
+\item {\tt Local Open Scope} {\scope}.
 
-\item {\tt Close Local Scope} {\scope}.
+\item {\tt Local Close Scope} {\scope}.
 
 These variants are not exported to the modules that import the module
 where they occur, even if outside a section.
@@ -743,13 +743,13 @@ is interpreted in the scope stack extended by the scopes bound (if any)
 to these arguments.
 
 \begin{Variants}
-\item {\tt Arguments Scope Global} {\qualid} {\tt [ \nelist{\optscope}{} ]}
+\item {\tt Global Arguments Scope} {\qualid} {\tt [ \nelist{\optscope}{} ]}
 
 This behaves like {\tt Arguments Scope} {\qualid} {\tt [
 \nelist{\optscope}{} ]} but survives when a section is closed instead
 of stopping working at section closing.
 
-\item {\tt Arguments Scope Local} {\qualid} {\tt [ \nelist{\optscope}{} ]}
+\item {\tt Local Arguments Scope} {\qualid} {\tt [ \nelist{\optscope}{} ]}
 
 This is a synonym of {\tt Arguments Scope} {\qualid} {\tt [
 \nelist{\optscope}{} ]}: if in a section, the effect of the command
@@ -973,7 +973,7 @@ abbreviation but at the time it is used. Especially, abbreviations can
 be bound to terms with holes (i.e. with ``\_''). The general syntax
 for abbreviations is
 \begin{quote}
-\texttt{Notation} \zeroone{{\tt Local}} {\ident} \sequence{\ident} {\ident} \texttt{:=} {\term} 
+\zeroone{{\tt Local}} \texttt{Notation} {\ident} \sequence{\ident} {\ident} \texttt{:=} {\term} 
  \zeroone{{\tt (only parsing)}}~\verb=.=
 \end{quote}
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index d806adea5..9ed2e650c 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3680,13 +3680,14 @@ adding transparency hints that make the network more constrained
 (c.f. \ref{HintTransparency}).
 
 \begin{Variants}
-\item\texttt{Hint Local} \textsl{hint\_definition} \texttt{:}
+\item\texttt{Local Hint} \textsl{hint\_definition} \texttt{:}
   \ident$_1$ \ldots\ \ident$_n$
   
   This is used to declare a hint database that must not be exported to the other
   modules that require and import the current module. Inside a
   section, the option {\tt Local} is useless since hints do not
   survive anyway to the closure of sections.
+
 \end{Variants}
 
 The general