diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-06 17:15:16 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-06 17:15:16 +0000 |
| commit | 371cc90e75226a2c4b8022860bc4bd09b3e6657a (patch) | |
| tree | 27bd98e8427df1c3e349823553027429d96458c1 | |
| parent | 3bbeb996b9c699eb841a7c56aa07c670fa7cea92 (diff) | |
Fixing #3056
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16566 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/refman/RefMan-mod.tex | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex index f4a90740c..505c1110c 100644 --- a/doc/refman/RefMan-mod.tex +++ b/doc/refman/RefMan-mod.tex @@ -190,7 +190,8 @@ Defines a module type {\ident} equal to {\modtype}. \end{Variants} -\subsection{\tt Declare Module {\ident} : {\modtype}} +\subsection{\tt Declare Module {\ident} : {\modtype} +\comindex{Declare Module}} Declares a module {\ident} of type {\modtype}. |