From 9bf1f84def4e7635dd5b81038e5d76ee2a77204e Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 22 May 2008 17:12:11 +0000
Subject: Strategy commands are now exported

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10971 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-oth.tex | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'doc/refman/RefMan-oth.tex')

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index afe31d0d2..9a17c0f3c 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -135,7 +135,8 @@ environment}\\
 \ref{Theorem}
 
 
-\subsection{\tt Strategy {\it level} [ \qualid$_1$ \dots \qualid$_n$ ].\comindex{Strategy}\label{Strategy}}
+\subsection{\tt Strategy {\it level} [ \qualid$_1$ \dots \qualid$_n$
+  ].\comindex{Strategy}\comindex{Local Strategy}\label{Strategy}}
 This command generalizes the behaviour of {\tt Opaque} and {\tt
   Transaparent} commands. It is used to fine-tune the strategy for
 unfolding constants, both at the tactic level and at the kernel
@@ -159,8 +160,10 @@ Levels can be one of the following (higher to lower):
   (behaves like $-\infty$)
 \end{description}
 
-The behaviour regarding sections and modules is the same as for the
-{\tt Transparent} command.
+These directives survive section and module closure, unless the
+command is prefixed by {\tt Local}. In the latter case, the behaviour
+regarding sections and modules is the same as for the {\tt
+  Transparent} and {\tt Opaque} commands.
 
 \subsection[\tt Search {\qualid}.]{\tt Search {\qualid}.\comindex{Search}}
 This command displays the name and type of all theorems of the current
-- 
cgit v1.2.3

