avancement

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

2 files changed, 7 insertions, 19 deletions

diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex
index 985c60bab..0f94da1c6 100755
--- a/doc/RefMan-pro.tex
+++ b/doc/RefMan-pro.tex
@@ -90,13 +90,9 @@ be {\ident}.  This command (and the following ones) can only be used
 if the original goal has been opened using the {\tt Goal} command.
 \item {\tt Save Theorem {\ident}.} \\
  {\tt Save Lemma {\ident}.} \\
-  Are equivalent to {\tt Save {\ident}.}
-\item {\tt Save Remark {\ident}.}\\
-  Defines the proved term as a constant that will not be accessible
-  without using a qualified name after the end of the current section.
-\item {\tt Save Fact {\ident}.}\\
-  Defines the proved term as a constant that will not be accessible
-  without using a qualified name after the closing of two levels of sectioning.
+ {\tt Save Remark {\ident}.}\\
+ {\tt Save Fact {\ident}.}\\
+  Are equivalent to {\tt Save {\ident}.} 
 \end{Variants}
 
 \subsection{\tt Theorem {\ident} : {\form}.}\comindex{Theorem}\label{Theorem}
@@ -119,17 +115,9 @@ as a {\tt Theorem}, the name {\ident} is known at all section levels:
 \item {\tt Lemma {\ident} : {\form}.}\comindex{Lemma}\\
   It is equivalent to {\tt Theorem {\ident} : {\form}.}
 \item {\tt Remark {\ident} : {\form}.}\comindex{Remark}\\
-  Analogous to {\tt Theorem} except that {\ident} will be accessible
-  only by a qualified name after closing the current section.
-%%%%% This is no longer true:
-% All proofs of persistent objects
-% (such as theorems) referring to {\ident} within the section will be
-% replaced by the proof of {\ident}.  
-\item {\tt Fact {\ident} : {\form}.}\comindex{Fact}\\
-  Analogous to {\tt Theorem} except that {\ident} is accessible by a
-  short name after closing the current section but 
-  will be accessible only by a qualified name after closing the
-  section which is above the current section. 
+  {\tt Fact {\ident} : {\form}.}\comindex{Fact}\\
+  Used to have a different meaning, but are now equivalent to {\tt
+  Theorem {\ident} : {\form}.} They are kept for compatibility.
 \item {\tt Definition {\ident} : {\form}.}
 \comindex{Definition}\\
   Analogous to {\tt Theorem}, intended to be used in conjunction with
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex
index 7a5c5eca4..229fb4524 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -18,7 +18,7 @@
 \fi
 
 
-\includeonly{RefMan-tac.v,RefMan-tacex.v}
+%\includeonly{RefMan-tac.v,RefMan-tacex.v}
 
 \input{./version.tex}
 \input{./macros.tex}% extension .tex pour htmlgen