diff options
Diffstat (limited to 'doc/refman/RefMan-syn.tex')
-rw-r--r-- | doc/refman/RefMan-syn.tex | 56 |
1 files changed, 40 insertions, 16 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 2b0d636e..ea3d55f2 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -345,7 +345,7 @@ Infix "/\" := and (at level 80, right associativity). \subsection{Reserving notations \label{ReservedNotation} -\comindex{ReservedNotation}} +\comindex{Reserved Notation}} A given notation may be used in different contexts. {\Coq} expects all uses of the notation to be defined at the same precedence and with the @@ -774,32 +774,57 @@ To bind a delimiting key to a scope, use the command \end{quote} \subsubsection{Binding arguments of a constant to an interpretation scope -\comindex{Arguments Scope}} +\comindex{Arguments}} It is possible to set in advance that some arguments of a given constant have to be interpreted in a given scope. The command is \begin{quote} -{\tt Arguments Scope} {\qualid} {\tt [ \nelist{\optscope}{} ]} +{\tt Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{} \end{quote} -where the list is a list made either of {\tt \_} or of a scope name. -Each scope in the list is bound to the corresponding parameter of -{\qualid} in order. When interpreting a term, if some of the +where the list is the list of the arguments of {\qualid} eventually +annotated with their {\scope}. Grouping round parentheses can +be used to decorate multiple arguments with the same scope. +{\scope} can be either a scope name or its delimiting key. For example +the following command puts the first two arguments of {\tt plus\_fct} +in the scope delimited by the key {\tt F} ({\tt Rfun\_scope}) and the +last argument in the scope delimited by the key {\tt R} ({\tt R\_scope}). + +\begin{coq_example*} +Arguments plus_fct (f1 f2)%F x%R. +\end{coq_example*} + +The {\tt Arguments} command accepts scopes decoration to all grouping +parentheses. In the following example arguments {\tt A} and {\tt B} +are marked as maximally inserted implicit arguments and are +put into the {\tt type\_scope} scope. + +\begin{coq_example*} +Arguments respectful {A B}%type (R R')%signature _ _. +\end{coq_example*} + +When interpreting a term, if some of the arguments of {\qualid} are built from a notation, then this notation is interpreted in the scope stack extended by the scopes bound (if any) to these arguments. +Arguments scopes can be cleared with the following command: + +\begin{quote} +{\tt Arguments {\qualid} : clear scopes} +\end{quote} + \begin{Variants} -\item {\tt Global Arguments Scope} {\qualid} {\tt [ \nelist{\optscope}{} ]} +\item {\tt Global Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{} -This behaves like {\tt Arguments Scope} {\qualid} {\tt [ -\nelist{\optscope}{} ]} but survives when a section is closed instead +This behaves like {\tt Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{} +but survives when a section is closed instead 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}{} ]} +\item {\tt Local Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{} -This behaves like {\tt Arguments Scope} {\qualid} {\tt [ - \nelist{\optscope}{} ]} but does not survive modules and files. +This behaves like {\tt Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{} +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. @@ -861,7 +886,7 @@ declared or defined constant. We give an overview of the scopes used in the standard library of {\Coq}. For a complete list of notations in each scope, use the -commands {\tt Print Scopes} or {\tt Print Scopes {\scope}}. +commands {\tt Print Scopes} or {\tt Print Scope {\scope}}. \subsubsection{\tt type\_scope} @@ -1047,7 +1072,8 @@ at the time of use of the abbreviation. %except that abbreviations are used for printing (unless the modifier %\verb=(only parsing)= is given) while syntactic definitions were not. -\section{Tactic Notations} +\section{Tactic Notations +\comindex{Tactic Notation}} Tactic notations allow to customize the syntax of the tactics of the tactic language\footnote{Tactic notations are just a simplification of @@ -1140,8 +1166,6 @@ places where a list of the underlying entry can be used: {\nterm{entry}} is either {\tt\small constr}, {\tt\small hyp}, {\tt\small integer} or {\tt\small int\_or\_var}. -% $Id: RefMan-syn.tex 13329 2010-07-26 11:05:39Z herbelin $ - %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" |