diff options
| -rw-r--r-- | contrib/xml/xmlcommand.mli | 26 | ||||
| -rw-r--r-- | contrib/xml/xmlentries.ml4 | 17 |
2 files changed, 2 insertions, 41 deletions
diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli index 6e43be9c2..68d038f04 100644 --- a/contrib/xml/xmlcommand.mli +++ b/contrib/xml/xmlcommand.mli @@ -25,7 +25,7 @@ (* 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 *) +(* Note: it is printed only (and directly) the most discharged available *) (* form of the definition (all the parameters are *) (* lambda-abstracted, but the object can still refer to variables) *) val print : Libnames.reference -> string option -> unit @@ -34,27 +34,3 @@ val print : Libnames.reference -> string option -> unit (* 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 - -(*CSC: untested, no more working or semantics unclear -(* 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 - -(* printLibrary identifier directory_name *) -(* where identifier is the qualified name of a library 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 library d *) -(* Note: the terms are printed in their uncooked form plus the informations *) -(* on the parameters of their most cooked form *) -val printLibrary : Libnames.qualid Util.located -> 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 -*) diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4 index da65de237..56f21b625 100644 --- a/contrib/xml/xmlentries.ml4 +++ b/contrib/xml/xmlentries.ml4 @@ -37,25 +37,10 @@ VERNAC ARGUMENT EXTEND filename | [ ] -> [ None ] END -(* Disk name *) - -VERNAC ARGUMENT EXTEND diskname -| [ "Disk" string(fn) ] -> [ Some fn ] -| [ ] -> [ None ] -END +(* Print XML and Show XML *) VERNAC COMMAND EXTEND Xml | [ "Print" "XML" filename(fn) global(id) ] -> [ Xmlcommand.print id fn ] | [ "Show" "XML" filename(fn) "Proof" ] -> [ Xmlcommand.show fn ] - -(* -| [ "Print" "XML" "All" ] -> [ Xmlcommand.printAll () ] - -| [ "Print" "XML" "Module" diskname(dn) global(id) ] -> - [ Xmlcommand.printLibrary id dn ] - -| [ "Print" "XML" "Section" diskname(dn) ident(id) ] -> - [ Xmlcommand.printSection id dn ] -*) END |