- Un peu de doc, préparation du CHANGES pour la release.

- Re-restriction de inversion (après la correction des bugs - et
  notamment du "Unknown meta" qui apparaissait parfois -, inversion
  devenait capable d'agir sur des buts non atomiques, ce qui crée
  quelques incompatibilités, typiquement dans CoRN où inversion est
  utilisé dans un rôle de discriminate; en attendant de voir, on
  revient à la sémantique initiale).
- Généralisation de Local/Global dans Implicit Arguments pour avoir un
  fonctionnement plus uniforme et plus facile à documenter.
- Code mort (clenv.ml).



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

1 files changed, 35 insertions, 1 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index de6b93b424..c19e01538c 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1183,6 +1183,23 @@ After the above declaration is issued, implicit arguments can just (and
 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}}
+
+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}}
+
+When in a module, tells not to activate the implicit arguments of
+{\qualid} declared by this commands to contexts that requires the
+module.
+
+\end{Variants}
+
 \Example
 \begin{coq_eval}
 Reset Initial.
@@ -1217,7 +1234,8 @@ implicit arguments of {\qualid}.
 {\Coq} can also automatically detect what are the implicit arguments
 of a defined object. The command is just
 \begin{quote}
-\tt Implicit Arguments {\qualid}.
+{\tt Implicit Arguments {\qualid}
+\comindex{Implicit Arguments}}
 \end{quote}
 The auto-detection is governed by options telling if strict,
 contextual, or reversible-pattern implicit arguments must be
@@ -1225,6 +1243,22 @@ considered or not (see
 Sections~\ref{SetStrictImplicit},~\ref{SetContextualImplicit},~\ref{SetReversiblePatternImplicit}
 and also~\ref{SetMaximalImplicitInsertion}).
 
+\begin{Variants}
+\item {\tt Implicit Arguments Global {\qualid}
+\comindex{Implicit Arguments Global}}
+
+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}}
+
+When in a module, tells not to activate the implicit arguments of
+{\qualid} computed by this declaration to contexts that requires the
+module.
+
+\end{Variants}
+
 \Example
 \begin{coq_eval}
 Reset Initial.