MAJ Opaque/Transparent, Qed/Defined

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

2 files changed, 26 insertions, 16 deletions

diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index e998b8488e..d491a9136a 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -1235,13 +1235,18 @@ understood as if it would have been given before the statements still to be
 proved. 
 \item {\tt Proof} is recommended but can currently be omitted. On the
 opposite, {\tt Qed} is mandatory to validate a proof.
+\item Proofs ended by {\tt Qed} are declared opaque (see \ref{Opaque})
+and cannot be unfolded by conversion tactics (see \ref{Conversion-tactics}).
+To be able to unfold a proof, you should end the proof by {\tt Defined}
+ (see below). 
 \end{Remarks}
 
 \begin{Variants}
 \item {\tt Proof} {\tt .} \dots {\tt Defined} {\tt .}\\
   \comindex{Proof}
-  Same as {\tt Proof} {\tt .} \dots {\tt Qed} {\tt .} but it is
-  intended to surround a definition built using the proof-editing mode.
+  Same as {\tt Proof} {\tt .} \dots {\tt Qed} {\tt .} but the proof is
+  then declared transparent (see \ref{Transparent}), which means it
+  can be unfolded in conversion tactics (see \ref{Conversion-tactics}).
 \item {\tt Proof} {\tt .} \dots {\tt Save.}\\
   Same as {\tt Proof} {\tt .} \dots {\tt Qed} {\tt .}
 \item {\tt Goal} \type \dots {\tt Save} \ident \\
@@ -1251,6 +1256,7 @@ opposite, {\tt Qed} is mandatory to validate a proof.
 \end{Variants}
 \comindex{Proof}
 \comindex{Qed}
+\comindex{Defined}
 \comindex{Save}
 \comindex{Goal}
 
diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex
index 5beb3d78d5..9497bb7d00 100644
--- a/doc/RefMan-oth.tex
+++ b/doc/RefMan-oth.tex
@@ -85,13 +85,15 @@ displayed as in \Coq\ terms.
 \SeeAlso chapter~\ref{Extraction}.
 
 \subsection{\tt Opaque \qualid$_1$ \dots \qualid$_n$.}
-\comindex{Opaque}\label{Opaque}
-This command forbids the unfolding of the constants {\qualid$_1$} \dots
-{\qualid$_n$} by tactics using $\delta$-conversion. Unfolding a constant
-is replacing it by its definition.
-
-By default, {\tt Theorem} and its alternatives are stamped as {\tt
-  Opaque}. This is to keep with the usual mathematical practice of
+\comindex{Opaque}\label{Opaque} This command forbids the unfolding of
+the constants {\qualid$_1$} \dots {\qualid$_n$} by 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
@@ -110,15 +112,19 @@ environment}\\
 
 \subsection{\tt Transparent \qualid$_1$ \dots \qualid$_n$.}
 \comindex{Transparent}\label{Transparent}
-This command is the converse of {\tt Opaque}. By default, {\tt
-  Definition} and {\tt Local} declare objects as {\tt Transparent}.
+This command is the converse of {\tt Opaque} and can only apply on constants originally defined as {\tt Transparent} to restore their initial behaviour 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 brutal and 
-not synchronous
+\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.
+can cause changes in tactic scripts behaviour.
+
+At section or module closing, a constant recovers the status it got at
+the time of its definition.
 
 %TODO: expliquer le rapport avec les sections
 
@@ -128,8 +134,6 @@ can cause changes in tactic scripts behavior.
 \item \errindex{The reference \qualid\ was not found in the current
 environment}\\
     There is no constant referred by {\qualid} in the environment.
-    Nevertheless, if you give the command \verb|Transparent foo bar.|
-    and if \texttt{bar} does not exist, \texttt{foo} is set opaque.
 \end{ErrMsgs}
 
 \SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing},