Improved the treatment of Local/Global options (noneffective Local on

Implicit Arguments, Arguments Scope and Coercion fixed, noneffective
Global in sections for Hints and Notation detected).

Misc. improvements (comments + interpretation of Hint Constructors +
dev printer for hint_db).



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

1 files changed, 7 insertions, 4 deletions

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 77eb29285..a5678eacf 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -747,13 +747,16 @@ to these arguments.
 
 This behaves like {\tt Arguments Scope} {\qualid} {\tt [
 \nelist{\optscope}{} ]} but survives when a section is closed instead
-of stopping working at section closing.
+of stopping working at section closing. Without the {\tt Global} modifier,
+the effect of the command stops when the section it belongs to ends.
 
 \item {\tt Local Arguments Scope} {\qualid} {\tt [ \nelist{\optscope}{} ]}
 
-This is a synonym of {\tt Arguments Scope} {\qualid} {\tt [
-\nelist{\optscope}{} ]}: if in a section, the effect of the command
-stops when the section it belongs to ends.
+This behaves like {\tt Arguments Scope} {\qualid} {\tt [
+    \nelist{\optscope}{} ]} but does not survive modules and files.
+Without the {\tt Local} modifier, the effect of the command is
+visible from within other modules or files.
+
 \end{Variants}