xml contribution created.

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

1 files changed, 40 insertions, 0 deletions

diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli
new file mode 100644
index 0000000000..96d01b27f6
--- /dev/null
+++ b/contrib/xml/xmlcommand.mli
@@ -0,0 +1,40 @@
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                     A tactic to print Coq objects in XML                   *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 17/11/1999                                 *)
+(*                                                                            *)
+(* This module defines a pretty-printer and the stream of commands to the pp  *)
+(*                                                                            *)
+(******************************************************************************)
+
+(* print id dest                                                          *)
+(*  where id   is the identifier (name) of a definition/theorem or of an  *)
+(*             inductive definition                                       *)
+(*  and   dest is either None (for stdout) or (Some filename)             *)
+(* pretty prints via Xml.pp the object whose identifier is id on dest     *)
+(* Note: it is printed only (and directly) the most cooked available      *)
+(*       form of the definition (all the parameters are                   *)
+(*       lambda-abstracted, but the object can still refer to variables)  *)
+val print : Names.identifier -> string option -> unit
+
+(* show dest                                                  *)
+(*  where dest is either None (for stdout) or (Some filename) *)
+(* pretty prints via Xml.pp the proof in progress on dest     *)
+val show : string option -> unit
+
+(* print All () prints what is the structure of the current environment of *)
+(* Coq. No terms are printed. Useful only for debugging                    *)
+val printAll : unit -> unit
+
+(* printModule identifier directory_name *)
+(*  where identifier     is the name of a module 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 module d                                                 *)
+(* 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