- Export de pattern_ident vers les ARGUMENT EXTEND and co.

- Extension du test de réversibilité acyclique des notations dures aux
  notations de type abbréviation (du genre inhabited A := A).
- Ajout options Local/Global à Transparent/Opaque.
- Retour au comportement 8.1 pour "move" (dependant par défaut et mot-clé 
  dependent retiré).



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

2 files changed, 31 insertions, 34 deletions

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 7c6bf7297..8bcffb4ff 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -886,19 +886,24 @@ computation of algebraic values, such as numbers, and for reflexion-based
 tactics. The commands to fine-tune the reduction strategies and the
 lazy conversion algorithm are described first.
 
-\subsection[\tt Opaque \qualid$_1$ \dots \qualid$_n$.]{\tt Opaque \qualid$_1$ \dots \qualid$_n$.\comindex{Opaque}\label{Opaque}} This command tells not to unfold
+\subsection[\tt Opaque \qualid$_1$ \dots \qualid$_n$.]{\tt Opaque \qualid$_1$ \dots \qualid$_n$.\comindex{Opaque}\label{Opaque}} 
+This command has an effect on unfoldable constants, i.e. 
+on constants defined by {\tt Definition} or {\tt Let} (with an explicit
+body), or by a command assimilated to a definition such as {\tt
+Fixpoint}, {\tt Program Definition}, etc, or by a proof ended by {\tt
+Defined}. The command tells not to unfold
 the constants {\qualid$_1$} \dots {\qualid$_n$} in tactics using
-$\delta$-conversion. Unfolding a constant is replacing it by its
-definition. {\tt Opaque} can only apply on constants originally
-defined as {\tt Transparent}.
-
-Constants defined by a proof ended by {\tt Qed} are automatically
-stamped as {\tt Opaque} and can no longer be considered as {\tt
-Transparent}. This is to keep with the usual mathematical practice of
-{\em proof irrelevance}: what matters in a mathematical development is
-the sequence of lemma statements, not their actual proofs. This
-distinguishes lemmas from the usual defined constants, whose actual
-values are of course relevant in general.
+$\delta$-conversion (unfolding a constant is replacing it by its
+definition).
+
+{\tt Opaque} has also on effect on the conversion algorithm of {\Coq},
+telling to delay the unfolding of a constant as later as possible in
+case {\Coq} has to check the conversion (see Section~\ref{conv-rules})
+of two distinct applied constants.
+
+The scope of {\tt Opaque} is limited to the current section, or
+current file, unless the variant {\tt Opaque Global \qualid$_1$ \dots
+\qualid$_n$} is used.
 
 \SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing},
 \ref{Theorem}
@@ -912,19 +917,21 @@ environment}\\
 \end{ErrMsgs}
 
 \subsection[\tt Transparent \qualid$_1$ \dots \qualid$_n$.]{\tt Transparent \qualid$_1$ \dots \qualid$_n$.\comindex{Transparent}\label{Transparent}}
-This command is the converse of {\tt Opaque} and can only apply on constants originally defined as {\tt Transparent} to restore their initial behavior after an {\tt Opaque} command.
-
-The constants automatically declared transparent are the ones defined by a proof ended by {\tt Defined}, or by a {\tt
-  Definition} or {\tt Local} with an explicit body.
-
-\Warning {\tt Transparent} and \texttt{Opaque} are not synchronous
-with the reset mechanism. If a constant was transparent at point A, if
-you set it opaque at point B and reset to point A, you return to state
-of point A with the difference that the constant is still opaque. This
-can cause changes in tactic scripts behavior.
+This command is the converse of {\tt Opaque} and it applies on
+unfoldable constants to restore their unfoldability after an {\tt
+Opaque} command.
+
+Note in particular that constants defined by a proof ended by {\tt
+Qed} are not unfoldable and {\tt Transparent} has no effect on
+them. This is to keep with the usual mathematical practice of {\em
+proof irrelevance}: what matters in a mathematical development is the
+sequence of lemma statements, not their actual proofs. This
+distinguishes lemmas from the usual defined constants, whose actual
+values are of course relevant in general.
 
-At section or module closing, a constant recovers the status it got at
-the time of its definition.
+The scope of {\tt Transparent} is limited to the current section, or
+current file, unless the variant {\tt Transparent Global \qualid$_1$
+\dots \qualid$_n$} is used.
 
 \begin{ErrMsgs}
 % \item \errindex{Can not set transparent.}\\
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index ca06e1d78..00e8a3ece 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -202,16 +202,6 @@ This moves {\ident} at the top of the local context (at the beginning of the con
 
 This moves {\ident} at the bottom of the local context (at the end of the context).
 
-\item {\tt move dependent {\ident$_1$} after {\ident$_2$}}\\
-      {\tt move dependent {\ident$_1$} before {\ident$_2$}}\\
-      {\tt move dependent {\ident$_1$} at top}\\
-      {\tt move dependent {\ident$_1$} at bottom}
-
-This moves {\ident$_1$} towards the specified place. All the
-hypotheses that recursively depend on, for a downwards move, or
-in, for an upwards move, the hypothesis {\ident$_1$} are moved
-too so as to respect the order of dependencies between hypotheses.
-
 \end{Variants}
 
 \begin{ErrMsgs}