diff options
Diffstat (limited to 'contrib/xml/xmlcommand.mli')
| -rw-r--r-- | contrib/xml/xmlcommand.mli | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli index 96d01b27f6..df1a9f8b42 100644 --- a/contrib/xml/xmlcommand.mli +++ b/contrib/xml/xmlcommand.mli @@ -38,3 +38,12 @@ val printAll : unit -> unit (* Note: the terms are printed in their uncooked form plus the informations *) (* on the parameters of their most cooked form *) val printModule : Names.identifier -> string option -> unit + +(* printSection identifier directory_name *) +(* where identifier is the name of a closed section d *) +(* and directory_name is the directory in which to root all the xml files *) +(* prints all the xml files and directories corresponding to the subsections *) +(* and terms of the closed section d *) +(* Note: the terms are printed in their uncooked form plus the informations *) +(* on the parameters of their most cooked form *) +val printSection : Names.identifier -> string option -> unit |