- 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

3 files changed, 62 insertions, 4 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 47409b9845..3bfe09c166 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -213,6 +213,7 @@
 \newcommand{\onemodbinding}{\textrm{\textsl{module\_binding}}}
 \newcommand{\modbindings}{\textrm{\textsl{module\_bindings}}}
 \newcommand{\qualid}{\textrm{\textsl{qualid}}}
+\newcommand{\qualidorstring}{\textrm{\textsl{qualid\_or\_string}}}
 \newcommand{\class}{\textrm{\textsl{class}}}
 \newcommand{\dirpath}{\textrm{\textsl{dirpath}}}
 \newcommand{\typedidents}{\textrm{\textsl{typed\_idents}}}
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.
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index f5bef115fd..a51e97d952 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -642,6 +642,12 @@ This does the same but uses the bindings in each {\bindinglist} to
 instantiate the parameters of the corresponding type of {\term}
 (see syntax of bindings in Section~\ref{Binding-list}).
 
+\item {\tt eapply \nelist{{\term} {\bindinglist}}{,} in {\ident}}
+
+This works as {\tt apply \nelist{{\term} {\bindinglist}}{,} in
+{\ident}} but turns unresolved bindings into existential variables, if
+any, instead of failing.
+
 \end{Variants}
 
 \subsection{\tt generalize \term
@@ -1086,6 +1092,19 @@ with its $\beta\iota$-normal form.
 
   \ErrMsg {\qualid}$_i$ {\tt does not occur}
 
+\item {\tt unfold {\qstring}}
+
+  If {\qstring} denotes the discriminating symbol of a notation (e.g. {\tt
+  "+"}) or an expression defining a notation (e.g. \verb!"_ + _"!), and
+  this notation refers to an unfoldable constant, then the tactic
+  unfolds it.
+
+\item {\tt unfold \qualidorstring$_1$ at \num$_1^1$, \dots, \num$_i^1$,
+\dots,\ \qualidorstring$_n$ at \num$_1^n$ \dots\ \num$_j^n$}
+
+  This is the most general form, where {\qualidorstring} is either a
+  {\qualid} or a {\qstring} referring to a notation.
+
 \end{Variants}
 
 \subsection{{\tt fold} \term
@@ -1980,6 +1999,11 @@ This happens if \term$_1$ does not occur in the goal.
     of $\term$ will be done, leading to failure if these $n$ rewrites are not possible. 
   \end{itemize}
 
+\item {\tt erewrite {\term}\tacindex{erewrite}}
+
+This tactic works as {\tt rewrite {\term}} but turning unresolved
+bindings into existential variables, if any, instead of failing. It has
+the same variants as {\tt rewrite} has.
 
 \end{Variants}
 
@@ -3596,6 +3620,7 @@ The tactic {\tt exists (n // m)} did not fail. The hole was solved by
 
 \section{Generation of induction principles with {\tt Scheme}
 \label{Scheme}
+\index{Schemes}
 \comindex{Scheme}}
 
 The {\tt Scheme} command is a high-level tool for generating
@@ -3624,7 +3649,7 @@ general principle of mutual induction for objects in type {\term$_i$}.
   Same as before but defines a non-dependent elimination principle more
   natural in case of inductively defined relations. 
 
-\item {\tt Scheme Equality for \ident$_1$}
+\item {\tt Scheme Equality for \ident$_1$\comindex{Scheme Equality}}
 
   Tries to generate a boolean equality and a proof of the
   decidability of the usual equality.
@@ -3658,8 +3683,6 @@ generates {\ident$_0$} to be the conjunction of the principles: it is
 built from the common premises of the principles and concluded by the
 conjunction of their conclusions.
 
-\SeeAlso \ref{CombinedScheme-examples}
-
 \SeeAlso Section~\ref{CombinedScheme-examples}
 
 \section{Generation of induction principles with {\tt Functional Scheme}