Documentation of the ! annotation for functor application

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

2 files changed, 12 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index a43ff34e43..a397d18099 100644
--- a/CHANGES
+++ b/CHANGES
@@ -172,6 +172,8 @@ Language
   \Delta-equivalence on qualified name. The include operator has been extended 
   to high-order structures (cf. libraries Numbers and Structures to see examples).
   Interactive proofs are now authorized in module type.
+  A functor application can be prefixed by a "!" to make it ignore any "Inline"
+  annotation in the type of its argument(s).
 
 Program
 
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
index 40fd6f1102..eff98d5882 100644
--- a/doc/refman/RefMan-mod.tex
+++ b/doc/refman/RefMan-mod.tex
@@ -12,6 +12,7 @@ together, as well as a mean of massive abstraction.
  & $|$ & {\modtype} \texttt{ with Definition }{\qualid} := {\term} \\
  & $|$ & {\modtype} \texttt{ with Module }{\qualid} := {\qualid} \\
  & $|$ & {\qualid} \nelist{\qualid}{}\\
+ & $|$ & $!${\qualid} \nelist{\qualid}{}\\
  &&\\
 
 {\onemodbinding}  & ::= & {\tt ( [Import|Export] \nelist{\ident}{} : {\modtype} )}\\
@@ -20,12 +21,17 @@ together, as well as a mean of massive abstraction.
 {\modbindings} & ::= & \nelist{\onemodbinding}{}\\
  &&\\
 
-{\modexpr} & ::= & \nelist{\qualid}{} 
+{\modexpr} & ::= & \nelist{\qualid}{} \\
+           & $|$ & $!$\nelist{\qualid}{}
 \end{tabular}
 \end{centerframe}
 \caption{Syntax of modules}
 \end{figure}
 
+In the syntax of module application, the $!$ prefix indicates that
+any {\tt Inline} directive in the type of the functor arguments
+will be ignored (see \ref{Inline} below).
+
 \subsection{\tt Module {\ident}
 \comindex{Module}}
 
@@ -144,6 +150,7 @@ This command is used to start an interactive module type {\ident}.
 \end{Variants}
 \subsubsection{Reserved commands inside an interactive module type:
 \comindex{Include}\comindex{Inline}}
+\label{Inline}
 \begin{enumerate}
 \item {\tt Include {\module}}
 
@@ -155,7 +162,8 @@ is a shortcut for {\tt Include {\module$_1$}}  $\ldots$ {\tt Include {\module$_n
 
 \item {\tt {\declarationkeyword} Inline {\assums} }
 
- This declaration will be automatically unfolded at functor application.
+ This declaration will be automatically unfolded at functor
+ application, except when this functor application is prefixed by a $!$ annotation.
 \end{enumerate}
 \subsection{\tt End {\ident}
 \comindex{End}}