From ff249870a9db77a6cbf20bcd839a346b2b749fec Mon Sep 17 00:00:00 2001 From: sacerdot Date: Wed, 25 Oct 2000 09:15:24 +0000 Subject: xml contribution created. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@756 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/xml/xmlcommand.mli | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 contrib/xml/xmlcommand.mli (limited to 'contrib/xml/xmlcommand.mli') 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 *) +(* 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 -- cgit v1.2.3