From 349087c4fcbfbbe81bdc3d8ea48291f84dc45af2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 28 Apr 2009 15:50:01 +0000
Subject: 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
---
 doc/refman/RefMan-oth.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc')

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}
-- 
cgit v1.2.3