diff options
Diffstat (limited to 'contrib/xml')
| -rw-r--r-- | contrib/xml/Xml.v | 46 | ||||
| -rw-r--r-- | contrib/xml/xmlentries.ml | 58 |
2 files changed, 0 insertions, 104 deletions
diff --git a/contrib/xml/Xml.v b/contrib/xml/Xml.v deleted file mode 100644 index 91fe6295ab..0000000000 --- a/contrib/xml/Xml.v +++ /dev/null @@ -1,46 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* A module to print Coq objects in XML *) -(* *) -(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *) -(* 06/12/2000 *) -(******************************************************************************) - -Declare ML Module "xml" "xmlcommand" "xmlentries". - -Grammar vernac vernac : ast := - xml_print [ "Print" "XML" tactic:qualidarg($id) "." ] -> - [(Print $id)] - -| xml_print_file [ "Print" "XML" "File" stringarg($fn) tactic:qualidarg($id) "." ] -> - [(Print $id $fn)] - -| xml_show [ "Show" "XML" "Proof" "." ] -> - [(Show)] - -| xml_show_file [ "Show" "XML" "File" stringarg($fn) "Proof" "." ] -> - [(Show $fn)] - -| xml_print_all [ "Print" "XML" "All" "." ] -> - [(XmlPrintAll)] - -| xml_print_module [ "Print" "XML" "Module" tactic:qualidarg($id) "." ] -> - [(XmlPrintModule $id)] - -| xml_print_module_disk [ "Print" "XML" "Module" "Disk" stringarg($dn) tactic:qualidarg($id) "." ] -> - [(XmlPrintModule $id $dn)] - -| xml_print_section [ "Print" "XML" "Section" identarg($id) "." ] -> - [(XmlPrintSection $id)] - -| xml_print_section_disk [ "Print" "XML" "Section" "Disk" stringarg($dn) identarg($id) "." ] -> - [(XmlPrintSection $id $dn)]. diff --git a/contrib/xml/xmlentries.ml b/contrib/xml/xmlentries.ml deleted file mode 100644 index 2323adaa0d..0000000000 --- a/contrib/xml/xmlentries.ml +++ /dev/null @@ -1,58 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* A module to print Coq objects in XML *) -(* *) -(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *) -(* 06/12/2000 *) -(* *) -(* This module adds to the vernacular interpreter the functions that fullfill *) -(* the new commands defined in Xml.v *) -(* *) -(******************************************************************************) - -open Util;; -open Vernacinterp;; - -vinterp_add "Print" - (function - [VARG_QUALID id] -> - (fun () -> Xmlcommand.print id None) - | [VARG_QUALID id ; VARG_STRING fn] -> - (fun () -> Xmlcommand.print id (Some fn)) - | _ -> anomaly "This should be trapped");; - -vinterp_add "Show" - (function - [] -> - (fun () -> Xmlcommand.show None) - | [VARG_STRING fn] -> - (fun () -> Xmlcommand.show (Some fn)) - | _ -> anomaly "This should be trapped");; - -vinterp_add "XmlPrintAll" - (function - [] -> (fun () -> Xmlcommand.printAll ()) - | _ -> anomaly "This should be trapped");; - -vinterp_add "XmlPrintModule" - (function - [VARG_QUALID id] -> (fun () -> Xmlcommand.printModule id None) - | [VARG_QUALID id ; VARG_STRING dn] -> - (fun () -> Xmlcommand.printModule id (Some dn)) - | _ -> anomaly "This should be trapped");; - -vinterp_add "XmlPrintSection" - (function - [VARG_IDENTIFIER id] -> (fun () -> Xmlcommand.printSection id None) - | [VARG_IDENTIFIER id ; VARG_STRING dn] -> - (fun () -> Xmlcommand.printSection id (Some dn)) - | _ -> anomaly "This should be trapped");; |