Backporting 11445 from 8.2 to trunk (negative conditions in

SearchAbout + referring objects by their notation).



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

1 files changed, 3 insertions, 3 deletions

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 22eb0eeae..967a8180a 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -713,13 +713,13 @@ ways to change the interpretation of subterms are available.
 \comindex{Delimit Scope}}
 
 It is possible to locally extend the interpretation scope stack using
-the syntax ({\term})\%{\nterm{key}} (or simply {\term}\%{\nterm{key}}
-for atomic terms), where {\nterm{key}} is a special identifier called
+the syntax ({\term})\%{\delimkey} (or simply {\term}\%{\delimkey}
+for atomic terms), where {\delimkey} is a special identifier called
 {\em delimiting key} and bound to a given scope.
 
 In such a situation, the term {\term}, and all its subterms, are
 interpreted in the scope stack extended with the scope bound to
-{\nterm{key}}.
+{\delimkey}.
 
 To bind a delimiting key to a scope, use the command