Backporting 12112 from v8.2 branch to trunk (fixing documentation bugs

#2099 in ConstructiveEpsilon.v and #2100 on Global Opaque).



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

1 files changed, 2 insertions, 2 deletions

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 0f6871f95e..cc6c4c483c 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -934,7 +934,7 @@ 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
+current file, unless the variant {\tt Global Opaque \qualid$_1$ \dots
 \qualid$_n$} is used.
 
 \SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing},
@@ -962,7 +962,7 @@ distinguishes lemmas from the usual defined constants, whose actual
 values are of course relevant in general.
 
 The scope of {\tt Transparent} is limited to the current section, or
-current file, unless the variant {\tt Transparent Global \qualid$_1$
+current file, unless the variant {\tt Global Transparent \qualid$_1$
 \dots \qualid$_n$} is used.
 
 \begin{ErrMsgs}