From 9bf1f84def4e7635dd5b81038e5d76ee2a77204e Mon Sep 17 00:00:00 2001 From: barras 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