Documentation Prop<=Set et Arguments Scope Global

Correction au passage d'un bug de Arguments Scope Global


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

2 files changed, 16 insertions, 0 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index dc7235ae6..6b8834526 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -422,6 +422,7 @@ convertibility into an order inductively defined by:
 \item if $i \leq j$ then $\WTEGLECONV{\Type(i)}{\Type(j)}$,
 \item for any $i$, $\WTEGLECONV{\Prop}{\Type(i)}$,
 \item for any $i$, $\WTEGLECONV{\Set}{\Type(i)}$,
+\item $\WTEGLECONV{\Prop}{\Set}$,
 \item if $\WTEGCONV{T}{U}$ and $\WTELECONV{\Gamma::(x:T)}{T'}{U'}$ then $\WTEGLECONV{\forall~x:T,T'}{\forall~x:U,U'}$.
 \end{enumerate}
 
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index e319bdbb1..22eb0eeae 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -742,6 +742,21 @@ arguments of {\qualid} are built from a notation, then this notation
 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}{} ]}
+
+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}{} ]}
+
+This is a synonym of {\tt Arguments Scope} {\qualid} {\tt [
+\nelist{\optscope}{} ]}: if in a section, the effect of the command
+stops when the section it belongs to ends.
+\end{Variants}
+
+
 \SeeAlso The command to show the scopes bound to the arguments of a
 function is described in Section~\ref{About}.