From aac2d2ac490492f8466e1d45ba0079de376fe25a Mon Sep 17 00:00:00 2001
From: Lionel Rieg
Date: Thu, 25 Jun 2015 14:58:25 +0200
Subject: Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"

---
 doc/refman/RefMan-syn.tex | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'doc')

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}}
 
-- 
cgit v1.2.3