Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"

1 files changed, 8 insertions, 1 deletions

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 37cbd1eac1..aabc8a8995 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -757,7 +757,8 @@ ways to change the interpretation of subterms are available.
 \subsubsection{Local opening of an interpretation scope 
 \label{scopechange}
 \index{\%}
-\comindex{Delimit Scope}}
+\comindex{Delimit Scope}
+\comindex{Undelimit Scope}}
 
 It is possible to locally extend the interpretation scope stack using
 the syntax ({\term})\%{\delimkey} (or simply {\term}\%{\delimkey}
@@ -774,6 +775,12 @@ To bind a delimiting key to a scope, use the command
 \texttt{Delimit Scope} {\scope} \texttt{with} {\ident} 
 \end{quote}
 
+To remove a delimiting key of a scope, use the command
+
+\begin{quote}
+\texttt{Undelimit Scope} {\scope}
+\end{quote}
+
 \subsubsection{Binding arguments of a constant to an interpretation scope
 \comindex{Arguments}}