Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.v

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

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");;