xml contribution created.

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

11 files changed, 1281 insertions, 0 deletions

diff --git a/contrib/xml/README b/contrib/xml/README
new file mode 100644
index 0000000000..00835fc8a6
--- /dev/null
+++ b/contrib/xml/README
@@ -0,0 +1,99 @@
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                     A tactic to print Coq objects in XML                   *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 22/11/1999                                 *)
+(******************************************************************************)
+
+This tactic is aimed to exporting a piece of Coq library in XML format.
+It adds a few new commands to the vernacular:
+
+ Print XML id.                     It prints in XML the object whose name is id
+                                   Only the most cooked available form of the
+                                   term is printed
+ Print XML File "filename" id.     It prints in XML the object whose name is id
+                                   on the file whose name is filename
+                                   Only the most cooked available form of the
+                                   term is printed
+ Show XML Proof.                   It prints in XML the current proof in
+                                   progress
+ Show XML File "filename" Proof.   It prints in XML the current proof in
+                                   progress on the file whose name is filename
+ Print XML Dir id.                 It prints recursively in XML the closed
+                                   section whose name is id. The terms are
+                                   printed in their uncooked form plus the
+                                   informations on the parameters of their
+                                   most cooked form
+ Print XML Dir Disk "dirname" id.  It prints recursively in XML the closed
+                                   section whose name is id rooting the dir
+                                   corresponding to the section to the dir
+                                   whose name is dirname.  The terms are
+                                   printed in their uncooked form plus the
+                                   informations on the parameters of their
+                                   most cooked form
+ Print XML All.                    It prints what is the structure of the
+                                   current environment of Coq. No terms are
+                                   printed. Useful only for debugging
+
+ If xmlcommand.ml is compiled with the configuration parameter verbose
+ set to true, then the verbosity of all the previous commands will be
+ increased, except the one of Print XML All (that is always very verbose :-)
+
+Important note (fixing the uris):
+ 
+ The previous new commands are all damaged because they produce xml files
+ in which all the uris to other xml files are broken (they are only suffixes
+ of the right uris). So, to fix the uris, you must use the script fix_uri.pl
+ giving to it on stdin all the filenames of the uris to repair. The script
+ will modify all the files fixing all the uris in them. An uri will be fixed
+ iff it is a reference to one of the files whose name has been given on stdin.
+
+How to compile:
+
+ Edit the configuration parameters at the very beginning of file xmlcommand.ml:
+  dtdname is the complete path-name of the dtd file
+  verbose if set to true, increases the verbosity of all the "Print something"
+           commands (useful only for debugging)
+ Then do "make clean ; make all ; make opt ; make install-library"
+
+The files forming the tactic are:
+
+ Xml.v                  It adds new grammar rules to Coq environment.
+ xmlentries.ml          Links the functions implementing the new commands to
+                        the grammar rules declared in Xml.v
+ xmlcommand.ml          Defines the functions that implements the new commands
+                        Uses ntrefiner.ml, cooking.ml and xml.ml
+                        Contains also some configuration parameters
+ ntrefiner.ml           This file is copied verbatim from the natural tactic
+                        and used to get informations on the proof in progress
+ cooking.ml             Contains a function that returns the list of the
+                        ingredients for cooking an uncooked term
+ xml.ml                 The definition of a pretty-printer for XML and the one
+                        of the stream of commands to the pp
+
+The files to export the standard library of Coq are:
+
+ provacoq.v             Loads one at a time all the provacoqXXX files
+ provacoqXxx.v	        If Loaded it exports the theory XXX of the standard
+                        library of Coq
+
+Other files useful to test the new commands:
+
+ prova.v                Declares and exports some objects; exports also the
+                        theories provastruct, provastruct2 e provastruct3
+ provastruct.v          An example theory
+ provastruct2.v         Another example theory
+ provastruct3.v         Yet another example theory
+
+Other files:
+
+ README	               This file
+ fix_uri.pl            The script that fixes the broken uris in the xml files
+ Makefile              Targets are "all", "opt", "clean" and "install-library"
+ .depend               The dependecies file used by make
+ mkdirs.sh             Make all the dirs needed to export the standard library
+                        of Coq via provacoq.v
+ examples              A simbolic link to the root of the exported library
diff --git a/contrib/xml/Xml.v b/contrib/xml/Xml.v
new file mode 100644
index 0000000000..c5ee6c836e
--- /dev/null
+++ b/contrib/xml/Xml.v
@@ -0,0 +1,33 @@
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                     A tactic to print Coq objects in XML                   *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 17/11/1999                                 *)
+(******************************************************************************)
+
+Declare ML Module "ntrefiner" "xml" "cooking" "xmlcommand" "xmlentries".
+
+Grammar vernac vernac : Ast :=
+  xml_print [ "Print" "XML" identarg($id) "." ] ->
+               [(Print $id)]
+
+| xml_print_file [ "Print" "XML" "File" stringarg($fn) identarg($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_dir [ "Print" "XML" "Module" identarg($id) "." ] ->
+               [(XmlPrintModule $id)]
+
+| xml_print_dir_disk [ "Print" "XML" "Module" "Disk" stringarg($dn) identarg($id) "." ] ->
+               [(XmlPrintModule $id $dn)].
diff --git a/contrib/xml/cooking.ml b/contrib/xml/cooking.ml
new file mode 100644
index 0000000000..19420ff46b
--- /dev/null
+++ b/contrib/xml/cooking.ml
@@ -0,0 +1,88 @@
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                     A tactic to print Coq objects in XML                   *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 02/12/1999                                 *)
+(*                                                                            *)
+(* This module compute the list of variables occurring in a term from the     *)
+(* term and the list of variables possibly occuring in it                     *)
+(*                                                                            *)
+(******************************************************************************)
+
+let get_depth_of_var vl v =
+ let rec aux n =
+  function
+     [] -> None
+   | (he::tl) -> if List.mem v he then Some n else aux (n + 1) tl
+ in
+  aux 0 vl
+;;
+
+exception CookingInternalError;;
+
+let string_of_vars_list =
+ let add_prefix n s = string_of_int n ^ ": " ^ s in
+ let rec aux =
+  function
+     [n,v] -> (n,v)
+   | (n,v)::tl ->
+      let (k,s) = aux tl in
+       if k = n then (k, v ^ " " ^ s) else (n, v ^ " " ^ add_prefix k s)
+   | [] -> raise CookingInternalError
+ in
+  function
+     [] -> ""
+   | vl -> let (k,s) = aux vl in add_prefix k s
+;;
+
+(*CSC commento sbagliato ed obsoleto *)
+(* If t is \v1. ... \vn.t' where v1, ..., vn are in the variable list vl then *)
+(* get_params_from_type vl t returns [v1; ...; vn]                            *)
+let get_params_from_type vl t =
+ let rec rget t l =
+  let module T = Term in
+  let module N = Names in
+   match T.kind_of_term t with
+      T.IsProd (N.Name id, _, target) ->
+       let id' = N.string_of_id id in
+        (match get_depth_of_var vl id' with
+            None   -> l
+          | Some n -> rget target ((n,id')::l)
+        )
+    | T.IsCast (term, _) -> rget term l
+    | _ -> l
+ in
+  let pl = List.rev (rget t []) in
+   string_of_vars_list pl
+   (*List.fold_right
+   (fun x i -> x ^ match i with "" -> "" | i' -> " " ^ i') pl ""*)
+;;
+
+(* add_cooking_information csp vl                               *)
+(*  when  csp is the section path of the most cooked object co  *)
+(*  and   vl  is the list of variables possibly occuring in co  *)
+(* returns the list of variables actually occurring in co       *)
+let add_cooking_information csp vl =
+(*
+ let module CT = Constrtypes in
+ let module N = Names in
+  let clobj = Lib.map_leaf (N.objsp_of csp) in
+  let ctag = Libobject.object_tag clobj in
+   match ctag with
+      "CONSTANT" ->
+         let (ccmap, _, _) = Environ.outConstant clobj in
+          let {CT.cONSTBODY=cval0 ;
+               CT.cONSTTYPE=ctyp} = Listmap.map ccmap N.CCI
+          in
+           get_params_from_type vl ctyp
+    | "MUTUALINDUCTIVE" ->
+         let (cmap, _) = Environ.outMutualInductive clobj in
+          let {CT.mINDPACKETS=packs} = Listmap.map cmap N.CCI in
+           let {CT.mINDARITY=arity} = packs.(0) in
+            get_params_from_type vl arity
+    | _ -> Std.anomaly "Cooking of an uncoockable term required"
+*) ""
+;;
diff --git a/contrib/xml/cooking.mli b/contrib/xml/cooking.mli
new file mode 100644
index 0000000000..6eb5b4330d
--- /dev/null
+++ b/contrib/xml/cooking.mli
@@ -0,0 +1,20 @@
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                     A tactic to print Coq objects in XML                   *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 17/11/1999                                 *)
+(*                                                                            *)
+(* This module compute the list of variables occurring in a term from the     *)
+(* term and the list of variables possibly occuring in it                     *)
+(*                                                                            *)
+(******************************************************************************)
+
+(* add_cooking_information csp vl                               *)
+(*  when  csp is the section path of the most cooked object co  *)
+(*  and   vl  is the list of variables possibly occuring in co  *)
+(* returns the list of variables actually occurring in co       *)
+val add_cooking_information :
+  Names.section_path -> string list list -> string
diff --git a/contrib/xml/ntrefiner.ml b/contrib/xml/ntrefiner.ml
new file mode 100644
index 0000000000..dd2b2ad942
--- /dev/null
+++ b/contrib/xml/ntrefiner.ml
@@ -0,0 +1,71 @@
+(**************************************************************************
+  *********                  ntrefiner.ml                          *********
+  **************************************************************************)
+
+(*
+open Std;;
+open Names;;
+open Generic;;
+open Term;;
+open Termenv;;
+open More_util;;
+open Proof_trees;;
+open Logic;;
+open Refiner;;
+open Evd;;
+
+
+(*the only difference with extract_open_proof is that the 
+  path of the unsolved goal in put in metavar assoc list 
+  extract_open_proof : constr signature -> proof
+  -> constr * (int * constr) list
+  takes a constr signature corresponding to global definitions
+  and a (not necessarly complete) proof
+  and gives a pair (pfterm,obl)
+  where pfterm is the constr corresponding to the proof
+  and obl is an int*constr list [ (m1,c1) ; ... ; (mn,cn)]
+  where the mi are metavariables numbers, and ci are their types.
+  Their proof should be completed in order to complete the initial proof*)
+let nt_extract_open_proof sign pf =
+ let open_obligations = ref [] in
+ let st = Stack.create () in
+ Stack.push 1 st;
+ let rec proof_extractor vl =
+  function
+     | {ref=Some ((PRIM _), _)} as pf -> prim_extractor proof_extractor vl pf
+     | {ref=Some ((TACTIC (str, _)), spfl); subproof=Some hidden_proof} ->
+      let sgl, v = frontier hidden_proof in
+      let flat_proof = v spfl in
+      if str = "Interpret" then (Stack.push 1 st);
+       let c = proof_extractor vl flat_proof in
+       if str = "Interpret" then
+        (Stack.pop st; Stack.push ((Stack.pop st) + 1) st); c
+     | {ref=Some ((CONTEXT ctxt), (pf :: []))} -> (proof_extractor vl) pf
+     | {ref=Some ((LOCAL_CONSTRAINTS lc), (pf :: []))} ->
+      (proof_extractor vl) pf
+     | {ref=None; goal=goal} ->
+      let visible_rels = map_succeed (function id ->
+       (match lookup_id id vl with
+       | GLOBNAME _ -> failwith "caught"
+       | RELNAME (n, _) -> n, id)) (ids_of_sign goal.hyps) in
+      let
+      sorted_rels = Sort.list (fun (n1, _) (n2, _) -> n1>n2) visible_rels
+      in
+      let
+      abs_concl =
+       List.fold_right
+       (fun (_, id) concl -> mkNamedProd id (snd (lookup_sign id goal.hyps)) concl)
+       sorted_rels goal.concl in
+      let path =
+       let l = ref [] in
+       let f i = l:=i::!l in
+       Stack.iter f st; List.tl !l in
+      Stack.push ((Stack.pop st) + 1) st;
+       let mv = newMETA () in
+       open_obligations:=(mv, (abs_concl, path))::!open_obligations;
+       applist (DOP0 (Meta mv), List.map (function n, _ -> Rel n) sorted_rels)
+     | _ -> error "ntrfiner__nt_extract_open_proof" in
+ let pfterm = proof_extractor (gLOB sign) pf in
+ pfterm, List.rev !open_obligations;;
+
+*)
diff --git a/contrib/xml/ntrefiner.mli b/contrib/xml/ntrefiner.mli
new file mode 100644
index 0000000000..1fb5bf1394
--- /dev/null
+++ b/contrib/xml/ntrefiner.mli
@@ -0,0 +1,13 @@
+(**************************************************************************
+  *********                  ntrefiner.ml                          *********
+  **************************************************************************)
+(*
+open Names;;
+open Term;;
+open Proof_trees;;
+
+
+val nt_extract_open_proof : 
+  constr signature -> proof_tree -> 
+    constr * (int * (constr * int list)) list;;
+*)
diff --git a/contrib/xml/xml.ml b/contrib/xml/xml.ml
new file mode 100644
index 0000000000..5cb3dbd06b
--- /dev/null
+++ b/contrib/xml/xml.ml
@@ -0,0 +1,72 @@
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                     A tactic to print Coq objects in XML                   *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 18/10/2000                                 *)
+(*                                                                            *)
+(* This module defines a pretty-printer and the stream of commands to the pp  *)
+(*                                                                            *)
+(******************************************************************************)
+
+
+(* the type token for XML cdata, empty elements and not-empty elements *)
+(* Usage:                                                                *)
+(*  Str cdata                                                            *)
+(*  Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen]   *)
+(*  NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *)
+(*          content                                                      *)
+type token = Str of string
+           | Empty of string * (string * string) list
+	   | NEmpty of string * (string * string) list * token Stream.t
+;;
+
+(* currified versions of the constructors make the code more readable *)
+let xml_empty name attrs = [< 'Empty(name,attrs) >]
+let xml_nempty name attrs content = [< 'NEmpty(name,attrs,content) >]
+let xml_cdata str = [< 'Str str >]
+
+(* Usage:                                                                   *)
+(*  pp tokens None     pretty prints the output on stdout                   *)
+(*  pp tokens (Some filename) pretty prints the output on the file filename *)
+let pp strm fn =
+ let channel = ref stdout in
+ let rec pp_r m =
+  parser
+    [< 'Str a ; s >] ->
+      print_spaces m ;
+      fprint_string (a ^ "\n") ;
+      pp_r m s
+  | [< 'Empty(n,l) ; s >] ->
+      print_spaces m ;
+      fprint_string ("<" ^ n) ;
+      List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l;
+      fprint_string "/>\n" ;
+      pp_r m s
+  | [< 'NEmpty(n,l,c) ; s >] ->
+      print_spaces m ;
+      fprint_string ("<" ^ n) ;
+      List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l;
+      fprint_string ">\n" ;
+      pp_r (m+1) c ;
+      print_spaces m ;
+      fprint_string ("</" ^ n ^ ">\n") ;
+      pp_r m s
+  | [< >] -> ()
+ and print_spaces m =
+  for i = 1 to m do fprint_string "  " done
+ and fprint_string str =
+  output_string !channel str
+ in
+  match fn with
+     Some filename ->
+       channel := open_out filename ;
+       pp_r 0 strm ;
+       close_out !channel ;
+       print_string ("\nWriting on file \"" ^ filename ^ "\" was succesfull\n");
+       flush stdout
+   | None ->
+       pp_r 0 strm
+;;
diff --git a/contrib/xml/xml.mli b/contrib/xml/xml.mli
new file mode 100644
index 0000000000..a82c582f69
--- /dev/null
+++ b/contrib/xml/xml.mli
@@ -0,0 +1,35 @@
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                     A tactic to print Coq objects in XML                   *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 18/10/2000                                 *)
+(*                                                                            *)
+(* This module defines a pretty-printer and the stream of commands to the pp  *)
+(*                                                                            *)
+(******************************************************************************)
+
+(* Tokens for XML cdata, empty elements and not-empty elements           *)
+(* Usage:                                                                *)
+(*  Str cdata                                                            *)
+(*  Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen]   *)
+(*  NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *)
+(*          content                                                      *)
+type token =
+  | Str of string
+  | Empty of string * (string * string) list
+  | NEmpty of string * (string * string) list * token Stream.t
+
+(* currified versions of the token constructors make the code more readable *)
+val xml_empty : string -> (string * string) list -> token Stream.t
+val xml_nempty :
+  string -> (string * string) list -> token Stream.t -> token Stream.t
+val xml_cdata : string -> token Stream.t
+
+(* The pretty printer for streams of token                                  *)
+(* Usage:                                                                   *)
+(*  pp tokens None     pretty prints the output on stdout                   *)
+(*  pp tokens (Some filename) pretty prints the output on the file filename *)
+val pp : token Stream.t -> string option -> unit
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
new file mode 100644
index 0000000000..4440c50637
--- /dev/null
+++ b/contrib/xml/xmlcommand.ml
@@ -0,0 +1,766 @@
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                     A tactic to print Coq objects in XML                   *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 02/12/1999                                 *)
+(*                                                                            *)
+(* This module defines the functions that implements the new commands         *)
+(*                                                                            *)
+(******************************************************************************)
+
+
+(* CONFIGURATION PARAMETERS *)
+
+let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
+let verbose = ref false;; (* always set to true during a "Print XML All" *)
+
+
+
+exception ImpossiblePossible;;
+type formal_parameters =
+   Actual of string
+ | Possible of string
+;;
+
+
+(* LOCAL MODULES *)
+
+(* Next local module because I can't use the standard module Str in a tactic, *)
+(* so I reimplement the part of it I need                                     *)
+module Str =
+ struct
+  exception WrongTermSuffix of string;;
+
+  (* substitute character c1 with c2 in string str *)
+  let rec substitute str c1 c2 =
+   try
+    let pos = String.index str c1 in
+     str.[pos] <- c2 ;
+     substitute str c1 c2
+   with
+    Not_found -> str ;;
+
+  (* change the suffix suf1 with suf2 in the string str *)
+  let change_suffix str suf1 suf2 =
+   let module S = String in
+    let len  = S.length str
+    and lens = S.length suf1 in
+     if S.sub str (len - lens) lens = suf1 then
+      (S.sub str 0 (len - lens)) ^ suf2
+     else
+      raise (WrongTermSuffix str) ;;
+ end
+;;
+
+(* UTILITY FUNCTIONS *)
+
+let print_if_verbose s = if !verbose then print_string s;;
+
+let ext_of_tag =
+ function
+    "CONSTANT"        -> "con"
+  | "MUTUALINDUCTIVE" -> "ind"
+  | "VARIABLE"        -> "var"
+  | _                 -> "err" (* uninteresting thing that won't be printed *)
+;;
+
+(* could_have_namesakes sp = true iff o is an object that could be cooked and *)
+(* than that could exists in cooked form with the same name in a super        *)
+(* section of the actual section                                              *)
+let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
+ let module D = Declare in
+  let tag = Libobject.object_tag o in
+   match tag with
+      "CONSTANT" ->
+        (match D.constant_strength sp with
+            D.DischargeAt _  -> false (* a local definition *)
+          | D.NeverDischarge -> true  (* a non-local one    *)
+        )
+    | "VARIABLE"        -> false  (* variables are local, so no namesakes     *)
+    | "MUTUALINDUCTIVE" -> true   (* mutual inductive types are never local   *)
+    | _                 -> false  (* uninteresting thing that won't be printed*)
+;;
+
+(* uri_of_path sp is a broken (wrong) uri pointing to the object whose        *)
+(* section path is sp                                                         *)
+let uri_of_path sp =
+(*CSCV7
+ let ext_of_sp sp =
+  let module N = Names in
+   try
+    let lobj = Lib.map_leaf (N.objsp_of sp) in
+    let tag = Libobject.object_tag lobj in
+     ext_of_tag tag
+   with _ -> Util.anomaly ("wrong search of term " ^ N.string_of_path sp)
+*) let ext_of_sp sp = "v7"
+ in
+  let module S = String in
+   let str = Names.string_of_path sp in
+    let uri = Str.substitute str '#' '/' in
+     let uri' = "cic:" ^ uri in
+      let uri'' = Str.change_suffix uri' ".cci" ("." ^ ext_of_sp sp) in
+       uri''
+;;
+
+let string_of_sort =
+ let module T = Term in
+  function
+     T.Prop(T.Pos)  -> "Set"
+   | T.Prop(T.Null) -> "Prop"
+   | T.Type(_)      -> "Type"
+;;
+
+let string_of_name =
+ let module N = Names in
+  function
+     N.Name id -> N.string_of_id id
+   | _         -> Util.anomaly "this should not happen"
+;;
+
+(* A SIMPLE DATA STRUCTURE AND SOME FUNCTIONS TO MANAGE THE CURRENT *)
+(* ENVIRONMENT (= [l1, ..., ln] WHERE li IS THE LIST OF VARIABLES   *)
+(* DECLARED IN THE i-th SUPER-SECTION OF THE CURRENT SECTION        *)
+
+(*CSC: commento sbagliato ed obsoleto *)
+(* list of variables availables in the actual section *)
+let pvars = ref [];;
+
+let pvars_to_string pvars =
+ let rec aux =
+  function
+     [] -> (0, "")
+   | he::tl -> 
+      let (n,s) = aux tl in
+       (n + 1,
+        string_of_int n ^ ": " ^ (String.concat " ") (List.rev he) ^
+         match s with "" -> "" | _ -> " " ^ s 
+       )
+ in
+  snd (aux (List.rev pvars))
+;;
+
+exception XmlCommandInternalError;;
+
+let add_to_pvars v =
+ match !pvars with
+    []       -> raise XmlCommandInternalError
+  | (he::tl) -> pvars := (v::he)::tl
+;;
+
+let get_depth_of_var v =
+ let rec aux n =
+  function
+     [] -> None
+   | (he::tl) -> if List.mem v he then Some n else aux (n + 1) tl
+ in
+  aux 0 !pvars
+;;
+
+(* FUNCTIONS TO CREATE IDENTIFIERS *)
+
+(* seed to create the next identifier *)
+let next_id = ref 0;;
+
+(* reset_id () reset the identifier seed to 0 *)
+let reset_id () =
+ next_id := 0
+;;
+
+(* get_next_id () returns fresh identifier *)
+let get_next_id () =
+ let res = 
+  "i" ^ string_of_int !next_id
+ in
+  incr next_id ;
+  res
+;;
+
+(* FUNCTION TO PRINT A SINGLE TERM OF CIC *)
+
+(* print_term t l where t is a term of Cic returns a stream of XML tokens *)
+(* suitable to be printed via the pretty printer Xml.pp. l is the list of *)
+(* bound names                                                            *)
+let print_term l csr =
+ let module N = Names in
+ let module T = Term in
+ let module X = Xml in
+  let rec names_to_ids =
+   function
+      [] -> []
+    | (N.Name id)::l -> id::(names_to_ids l)
+    | _ -> names_to_ids l
+  in
+  let rec term_display l cstr =
+   (* kind_of_term helps doing pattern matching hiding the lower level of *)
+   (* coq coding of terms (the one of the logical framework)              *)
+   match T.kind_of_term cstr with
+     T.IsRel n  ->
+      (match List.nth l (n - 1) with
+          N.Name id ->
+            X.xml_empty "REL"
+             ["value",(string_of_int n) ;
+              "binder",(N.string_of_id id) ;
+              "id", get_next_id ()]
+        | N.Anonymous -> raise XmlCommandInternalError
+     )
+   | T.IsVar id ->
+      let depth =
+       match get_depth_of_var (N.string_of_id id) with
+          None -> "?" (* when printing via Show XML Proof or Print XML id *)
+                      (* no infos about variables uri are known           *)
+        | Some n -> string_of_int n
+      in
+       X.xml_empty "VAR"
+        ["relUri",depth ^ "," ^ (N.string_of_id id) ;
+         "id", get_next_id ()]
+   | T.IsMeta n ->
+      X.xml_empty "META" ["no",(string_of_int n) ; "id", get_next_id ()]
+   | T.IsSort s ->
+      X.xml_empty "SORT" ["value",(string_of_sort s) ; "id", get_next_id ()]
+   | T.IsCast (t1,t2) ->
+      X.xml_nempty "CAST" ["id", get_next_id ()]
+       [< X.xml_nempty "term" [] (term_display l t1) ;
+          X.xml_nempty "type" [] (term_display l t2)
+       >]
+   | T.IsLetIn (nid,s,_,d)->
+      let nid' = N.next_name_away nid (names_to_ids l) in
+       X.xml_nempty "LETIN" ["id", get_next_id ()]
+        [< X.xml_nempty "term" [] (term_display l s) ;
+           X.xml_nempty "target" ["binder",(N.string_of_id nid')]
+            (term_display ((N.Name nid')::l) d)
+        >]
+   | T.IsProd (N.Name _ as nid, t1, t2) ->
+      let nid' = N.next_name_away nid (names_to_ids l) in
+       X.xml_nempty "PROD" ["id", get_next_id ()]
+        [< X.xml_nempty "source" [] (term_display l t1) ;
+           X.xml_nempty "target" ["binder",(N.string_of_id nid')]
+            (term_display ((N.Name nid')::l) t2)
+        >]
+   | T.IsProd (N.Anonymous as nid, t1, t2) ->
+      X.xml_nempty "PROD" ["id", get_next_id ()]
+       [< X.xml_nempty "source" [] (term_display l t1) ;
+          X.xml_nempty "target" [] (term_display (nid::l) t2)
+       >]
+   | T.IsLambda (N.Name _ as nid, t1, t2) ->
+      let nid' = N.next_name_away nid (names_to_ids l) in
+       X.xml_nempty "LAMBDA" ["id", get_next_id ()]
+        [< X.xml_nempty "source" [] (term_display l t1) ;
+           X.xml_nempty "target" ["binder",(N.string_of_id nid')]
+            (term_display ((N.Name nid')::l) t2)
+        >]
+   | T.IsLambda (N.Anonymous as nid, t1, t2) ->
+      X.xml_nempty "LAMBDA" ["id", get_next_id ()]
+       [< X.xml_nempty "source" [] (term_display l t1) ;
+          X.xml_nempty "target" [] (term_display (nid::l) t2) >]
+   | T.IsApp (h,t) ->
+      X.xml_nempty "APPLY" ["id", get_next_id ()]
+       [< (term_display l h) ;
+          (Array.fold_right (fun x i -> [< (term_display l x) ; i >]) t [<>])
+       >]
+   | T.IsConst (sp,_) ->
+      X.xml_empty "CONST" ["uri",(uri_of_path sp) ; "id", get_next_id ()]
+   | T.IsMutInd ((sp,i),_) ->
+      X.xml_empty "MUTIND"
+       ["uri",(uri_of_path sp) ;
+        "noType",(string_of_int i) ;
+        "id", get_next_id ()]
+   | T.IsMutConstruct (((sp,i),j),_) ->
+      X.xml_empty "MUTCONSTRUCT"
+       ["uri",(uri_of_path sp) ;
+        "noType",(string_of_int i) ;
+        "noConstr",(string_of_int j) ;
+        "id", get_next_id ()]
+   | T.IsMutCase ((_,((sp,i),_,_,_,_)),ty,term,a) ->
+      let (uri, typeno) = (uri_of_path sp),i in
+       X.xml_nempty "MUTCASE"
+        ["uriType",uri ; "noType",(string_of_int typeno) ; "id",get_next_id ()]
+        [< X.xml_nempty "patternsType" [] [< (term_display l ty) >] ;
+	   X.xml_nempty "inductiveTerm" [] [< (term_display l term) >] ;
+	   Array.fold_right
+            (fun x i ->
+              [< X.xml_nempty "pattern" [] [< term_display l x >] ; i>]
+            ) a [<>]
+        >]
+   | T.IsFix ((ai,i),(t,f,b)) ->
+      X.xml_nempty "FIX" ["noFun", (string_of_int i) ; "id",get_next_id ()]
+       [< Array.fold_right
+           (fun (fi,ti,bi,ai) i ->
+             [< X.xml_nempty "FixFunction"
+                 ["name", (string_of_name fi); "recIndex", (string_of_int ai)]
+	         [< X.xml_nempty "type" [] [< term_display l ti >] ;
+	            X.xml_nempty "body" [] [< term_display ((List.rev f)@l) bi >]
+	         >] ;
+                i
+             >]
+           )
+	   (Array.mapi (fun j x -> (x,t.(j),b.(j),ai.(j)) ) (Array.of_list f) )
+           [<>]
+       >]
+   | T.IsCoFix (i,(t,f,b)) ->
+      X.xml_nempty "COFIX" ["noFun", (string_of_int i) ; "id",get_next_id ()]
+       [< Array.fold_right
+           (fun (fi,ti,bi) i ->
+            [< X.xml_nempty "CofixFunction" ["name", (string_of_name fi)]
+	        [< X.xml_nempty "type" [] [< term_display l ti >] ;
+	           X.xml_nempty "body" [] [< term_display ((List.rev f)@l) bi >]
+	        >] ;
+               i
+            >]
+	   )
+	   (Array.mapi (fun j x -> (x,t.(j),b.(j)) ) (Array.of_list f) ) [<>]
+       >]
+   | T.IsXtra _ ->
+      Util.anomaly "Xtra node in a term!!!"
+   | T.IsEvar _ ->
+      Util.anomaly "Evar node in a term!!!"
+  in
+    (*CSC: ad l vanno andrebbero aggiunti i nomi da non *)
+    (*CSC: mascherare (costanti? variabili?)            *)
+    term_display l csr
+;;
+
+(* FUNCTIONS TO PRINT A SINGLE OBJECT OF COQ *)
+
+(* print_current_proof term type id conjectures                            *)
+(*  where term        is the term of the proof in progress p               *)
+(*  and   type        is the type of p                                     *)
+(*  and   id          is the identifier (name) of p                        *)
+(*  and   conjectures is the list of conjectures (cic terms)               *)
+(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
+let print_current_proof c typ id mv =
+ let module X = Xml in
+  reset_id () ;
+  [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+     X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
+     X.xml_nempty "CurrentProof" ["name",id ; "id", get_next_id ()]
+       [< List.fold_right
+           (fun (j,t) i ->
+             [< X.xml_nempty "Conjecture" ["no",(string_of_int j)]
+                 [< print_term [] t >] ; i >])
+           mv [<>] ;
+          X.xml_nempty "body" [] [< print_term [] c >] ;
+          X.xml_nempty "type"  [] [< print_term [] typ >]
+       >]
+  >]
+;;
+
+(* print_axiom id type params                                              *)
+(*  where type        is the type of an axiom a                            *)
+(*  and   id          is the identifier (name) of a                        *)
+(*  and   params      is the list of formal params for a                   *)
+(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
+let print_axiom id typ fv =
+ let module X = Xml in
+ let module N = Names in
+  reset_id () ;
+  [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+     X.xml_cdata ("<!DOCTYPE Axiom SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
+     X.xml_nempty "Axiom"
+      (["name",(N.string_of_id id) ; "id", get_next_id ()] @
+       match fv with
+          Possible _ -> raise ImpossiblePossible
+        | Actual fv' -> ["params",fv']
+      ) [< X.xml_nempty "type" [] (print_term [] typ) >]
+  >]
+;;
+
+(* print_definition id term type params                                    *)
+(*  where id          is the identifier (name) of a definition d           *)
+(*  and   term        is the term (body) of d                              *)
+(*  and   type        is the type of d                                     *)
+(*  and   params      is the list of formal params for d                   *)
+(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
+let print_definition id c typ fv =
+ let module X = Xml in
+ let module N = Names in
+  reset_id () ;
+  [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+     X.xml_cdata ("<!DOCTYPE Definition SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
+     X.xml_nempty "Definition"
+      (["name",(N.string_of_id id) ; "id", get_next_id ()] @
+       match fv with
+          Possible fv' -> ["params",fv' ; "paramMode","POSSIBLE"]
+        | Actual fv' -> ["params",fv'])
+      [< X.xml_nempty "body" [] (print_term [] c) ;
+         X.xml_nempty "type"  [] (print_term [] typ) >]
+  >]
+;;
+
+(* print_variable id type                                                  *)
+(*  where id          is the identifier (name) of a variable v             *)
+(*  and   type        is the type of v                                     *)
+(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
+let print_variable id typ =
+ let module X = Xml in
+ let module N = Names in
+  reset_id () ;
+  [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+     X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
+     X.xml_nempty "Variable" ["name",(N.string_of_id id) ; "id", get_next_id ()]
+      (X.xml_nempty "type" [] (print_term [] typ))
+  >]
+;;
+
+(* print_mutual_inductive_packet p                                           *)
+(*  where p is a mutual inductive packet (an inductive definition in a block *)
+(*          of mutual inductive definitions)                                 *)
+(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp   *)
+(* Used only by print_mutual_inductive                                       *)
+let print_mutual_inductive_packet names p =
+ let module D = Declarations in
+ let module N = Names in
+ let module T = Term in
+ let module X = Xml in
+  let {D.mind_consnames=consnames ;
+       D.mind_typename=typename ;
+       D.mind_nf_lc=lc ;
+       D.mind_nf_arity=arity ;
+       D.mind_finite=finite} = p
+  in
+   [< X.xml_nempty "InductiveType"
+       ["name",(N.string_of_id typename) ;
+        "inductive",(string_of_bool finite)
+       ]
+       [<
+          X.xml_nempty "arity" [] (print_term [] (T.body_of_type arity)) ;
+          (Array.fold_right
+           (fun (name,lc) i ->
+             [< X.xml_nempty "Constructor" ["name",(N.string_of_id name)]
+                 (print_term names lc) ;
+                i
+             >])
+	   (Array.mapi (fun j x -> (x,T.body_of_type lc.(j)) ) consnames )
+           [<>]
+          )
+       >]
+   >]
+;;
+
+(* print_mutual_inductive packs params nparams                             *)
+(*  where packs       is the list of inductive definitions in the block of *)
+(*                    mutual inductive definitions b                       *)
+(*  and   params      is the list of formal params for b                   *)
+(*  and   nparams     is the number of "parameters" in the arity of the    *)
+(*                    mutual inductive types                               *)
+(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
+let print_mutual_inductive packs fv nparams =
+ let module D = Declarations in
+ let module X = Xml in
+ let module N = Names in
+  let names =
+   List.map
+    (fun p -> let {D.mind_typename=typename} = p in N.Name(typename))
+    (Array.to_list packs)
+  in
+   reset_id () ;
+   [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+      X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
+       dtdname ^ "\">\n\n") ;
+      X.xml_nempty "InductiveDefinition"
+       (["noParams",string_of_int nparams ; "id",get_next_id ()] @
+        (match fv with
+            Possible fv' -> ["params",fv' ; "paramMode","POSSIBLE"]
+          | Actual fv' -> ["params",fv']))
+       [< (Array.fold_right
+            (fun x i -> [< print_mutual_inductive_packet names x ; i >])
+            packs
+            [< >]
+          )
+       >]
+   >]
+;;
+
+(* 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)  *)
+let print id fn =
+ let module D = Declarations in
+ let module G = Global in
+ let module N = Names in
+ let module T = Term in
+ let module X = Xml in
+  let str = N.string_of_id id in
+  let sp = Nametab.sp_of_id N.CCI id in
+  let pp_cmds =
+   begin
+    try
+     let {D.const_body=val0 ; D.const_type = typ} = G.lookup_constant sp in
+     let typ = T.body_of_type typ in
+      begin
+       match val0 with
+          None -> print_axiom id typ (Actual "")
+        | Some lcvr ->
+           match !lcvr with
+              D.Cooked c -> print_definition id c typ (Actual "")
+            | D.Recipe _ ->
+               print_string " COOKING THE RECIPE\n" ;
+               ignore (D.cook_constant lcvr) ;
+               let {D.const_body=val0 ; D.const_type = typ} =
+                G.lookup_constant sp in
+               let typ = T.body_of_type typ in
+                begin
+                 match val0 with
+                   Some {contents= D.Cooked c} ->
+                    print_definition id c typ (Actual "")
+                 | _ -> Util.error "COOKING FAILED"
+                end
+          end
+    with
+     Not_found ->
+      try
+       let {D.mind_packets=packs ; D.mind_nparams=nparams} =
+        G.lookup_mind sp
+       in
+        print_mutual_inductive packs (Actual "") nparams
+      with
+       Not_found ->
+        Util.anomaly ("print: this should not happen")
+   end
+  in
+   Xml.pp pp_cmds fn
+;;
+ 
+(* show dest                                                  *)
+(*  where dest is either None (for stdout) or (Some filename) *)
+(* pretty prints via Xml.pp the proof in progress on dest     *)
+let show fn =
+(*
+ let pftst = Pfedit.get_pftreestate () in
+ let id = Pfedit.get_proof () in
+ let pf = Tacmach.proof_of_pftreestate pftst in
+ let typ = (Proof_trees.goal_of_proof pf).Evd.concl in
+ (*CSC: ntrefiner copied verbatim from natural, used, but _not_ understood *)
+ let val0, mv = Ntrefiner.nt_extract_open_proof (Vartab.initial_sign ()) pf in
+ let mv_t = List.map (function i, (t, _) -> i,t) mv in
+  Xml.pp (print_current_proof val0 typ id mv_t) fn
+*) ()
+;;
+
+(* FUNCTIONS TO PRINT AN ENTIRE SECTION OF COQ *)
+
+(* list of (name, uncooked sp, most cooked sp, uncooked leaf object,  *)
+(*          list of possible variables, directory name)               *)
+(* used to collect informations on the uncooked and most cooked forms *)
+(* of objects that could be cooked (have namesakes)                   *)
+let toprint = ref [];;
+
+(* makes a filename from a directory name, a section path and an extension *)
+let mkfilename dn sp ext =
+ let rec join_dirs cwd =
+   function
+      [] -> ""
+    | he::tail ->
+       let newcwd = cwd ^ "/" ^ he in
+        (try
+          Unix.mkdir newcwd 0o775
+         with _ -> () (* Let's ignore the errors on mkdir *)
+        ) ;
+        he ^ "/" ^ join_dirs newcwd tail
+ in
+  let module N = Names in
+   match dn with
+      None         -> None
+    | Some basedir ->
+       let (dirs, filename, _) = N.repr_path sp in
+        let dirs = List.rev dirs in (* misteries of Coq *)
+         Some (basedir ^ "/" ^ join_dirs basedir dirs ^
+               N.string_of_id filename ^ "." ^ ext ^ ".xml")
+;;
+
+(* Next exception is used only inside print_object *)
+exception Uninteresting;;
+
+(* print_object leaf_object id section_path directory_name formal_vars      *)
+(*  where leaf_object    is a leaf object                                   *)
+(*  and   id             is the identifier (name) of the definition/theorem *)
+(*                       or of the inductive definition o                   *)
+(*  and   section_path   is the section path of o                           *)
+(*  and   directory_name is the base directory in which putting the print   *)
+(*  and   formal_vars    is the list of parameters (variables) of o         *)
+(* pretty prints via Xml.pp the object o in the right directory deduced     *)
+(* from directory_name and section_path                                     *)
+(* Note: it is printed only the uncooked available form of the object plus  *)
+(*       the list of parameters of the object deduced from it's most cooked *)
+(*       form                                                               *)
+let print_object o id sp dn fv =
+ let module D = Declarations in
+ let module G = Global in
+ let module N = Names in
+ let module T = Term in
+ let module X = Xml in
+  let lobj = o in
+  let tag = Libobject.object_tag lobj in
+  let pp_cmds () =
+   match tag with
+      "CONSTANT" ->
+         (*CSC: QUI CI SONO ANCHE LE VARIABILI, CREDO, CHIAMATE const_hyps *)
+         let {D.const_body=val0 ; D.const_type = typ} = G.lookup_constant sp in
+         let typ = T.body_of_type typ in
+          begin
+           match val0 with
+              None -> print_axiom id typ fv
+            | Some lcvr ->
+               match !lcvr with
+                  D.Cooked c -> print_definition id c typ fv
+                | D.Recipe _ -> Util.anomaly "trying to print a recipe"
+          end
+    | "MUTUALINDUCTIVE" ->
+         (*CSC: QUI CI SONO ANCHE LE VARIABILI, CREDO, CHIAMATE mind_hyps *)
+         let {D.mind_packets=packs ; D.mind_nparams=nparams} =
+          G.lookup_mind sp
+         in
+           print_mutual_inductive packs fv nparams
+    | "VARIABLE" ->
+        (*CHE COSA E' IL PRIMO ARGOMENTO?*)
+        let (_,typ) = G.lookup_named id in
+         add_to_pvars (N.string_of_id id) ;
+         print_variable id (T.body_of_type typ)
+    | "CLASS"
+    | "COERCION"
+    | _ -> raise Uninteresting
+  and fileext = ext_of_tag tag
+  in
+   try
+    Xml.pp (pp_cmds ()) (mkfilename dn sp fileext)
+   with
+    Uninteresting -> ()
+;;
+
+(* print_library_segment state bprintleaf directory_name                      *)
+(*  where state          is a list of (section-path, node)                    *)
+(*  and   bprintleaf     is true iff the leaf objects should be printed       *)
+(*  and   directory_name is the name of the base directory in which to print  *)
+(*                       the files                                            *)
+(* print via print_node all the nodes (leafs excluded if bprintleaf is false) *)(* in state                                                                   *)
+let rec print_library_segment state bprintleaf dn =
+  List.iter
+   (function (sp, node) ->
+     print_if_verbose (Names.string_of_path sp ^ "\n") ;
+     print_node node (Names.basename sp) sp bprintleaf dn ;
+     print_if_verbose "\n"
+   ) state
+(* print_node node id section_path bprintleaf directory_name             *)
+(* prints a single node (and all it's subnodes via print_library_segment *)
+and print_node n id sp bprintleaf dn =
+ let module L = Lib in
+  match n with
+     L.Leaf o ->
+      print_if_verbose "LEAF\n" ;
+      if bprintleaf then
+       begin
+        let to_print =
+         try
+          let _ =
+           List.find (function (x,_,_,_,_,_) -> x=id) !toprint
+          in
+           false
+         with Not_found -> true
+        in
+         if to_print then
+          (* this is an uncooked term or a local (with no namesakes) term *)
+          begin
+           if could_have_namesakes o sp then
+            (* this is an uncooked term *)
+            toprint := (id,sp,sp,o,!pvars,dn)::!toprint
+           else
+            (* this is a local term *)
+            print_object o id sp dn (Possible (pvars_to_string !pvars)) ;
+            print_if_verbose ("OK, stampo " ^ Names.string_of_id id ^ "\n")
+          end
+         else
+          (* update the least cooked sp *)
+          toprint :=
+           List.map
+            (function
+               (id',usp,_,uo,pv,dn) when id' = id -> (id,usp,sp,uo,pv,dn)
+             | t -> t
+            ) !toprint
+       end
+   | L.OpenedSection s -> print_if_verbose ("OpenDir " ^ s ^ "\n")
+   | L.ClosedSection (s,state) ->
+      print_if_verbose("ClosedDir " ^ s ^ "\n") ;
+      if bprintleaf then
+       begin
+        (* open a new scope *)
+        pvars := []::!pvars ;
+        print_library_segment state bprintleaf dn ;
+        (* close the scope *)
+        match !pvars with
+           [] -> raise XmlCommandInternalError
+         | he::tl -> pvars := tl
+       end ;
+      print_if_verbose "/ClosedDir\n"
+   | L.Module s ->
+      print_if_verbose ("Module " ^ s ^ "\n")
+   | L.FrozenState _ ->
+      print_if_verbose ("FrozenState\n")
+;;
+
+(* print_closed_section module_name node directory_name                      *)
+(*  where module_name is the name of a module                                *)
+(*  and   node is the library segment of the module                          *)
+(*  and   directory_name is the base directory in which to put the xml files *)
+(* prints all the leaf objects of the tree rooted in node using              *)
+(* print_library_segment on all its sons                                     *)
+let print_closed_section s ls dn =
+ let module L = Lib in
+ let module C = Cooking in
+  toprint := [] ;
+  (*CSC: this should always be empty yet! But just to be sure... :-) *)
+  pvars := [] ;
+  print_if_verbose ("Module " ^ s ^ ":\n") ;
+  print_library_segment ls true dn ;
+  print_if_verbose "\nNow saving cooking information: " ;
+  List.iter
+   (function
+      (id,usp,csp,uo,pv,dn) ->
+       print_if_verbose ("\nCooked=" ^ (Names.string_of_path csp) ^
+        "\tUncooked=" ^ (Names.string_of_path usp)) ;
+       let formal_vars = C.add_cooking_information csp pv in
+        pvars := pv ;
+        (*CSC Actual was Some *)
+        print_object uo id usp dn (Actual formal_vars)
+   ) !toprint ;
+  print_if_verbose "\n/Module\n" ;
+;;
+
+(* printModule identifier directory_name                                     *)
+(*  where identifier     is the name of a module (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 module d                                                 *)
+(* Note: the terms are printed in their uncooked form plus the informations  *)
+(* on the parameters of their most cooked form                               *)
+let printModule id dn =
+ let module L = Library in
+ let module N = Names in
+ let module X = Xml in
+  let str = N.string_of_id id in 
+  let sp = Lib.make_path id N.OBJ in
+  let ls = L.module_segment (Some str) in
+   print_if_verbose ("MODULE_BEGIN " ^ str ^ " " ^ N.string_of_path sp ^ " " ^
+    L.module_filename str ^ "\n") ;
+   print_closed_section str ls dn ;
+   print_if_verbose ("MODULE_END " ^ str ^ " " ^ N.string_of_path sp ^ " " ^
+    L.module_filename str ^ "\n")
+;;
+
+(* print All () prints what is the structure of the current environment of *)
+(* Coq. No terms are printed. Useful only for debugging                    *)
+let printAll () =
+ let state = Library.module_segment None in
+  let oldverbose = !verbose in
+   verbose := true ;
+   print_library_segment state false None ;
+   let ml = Library.loaded_modules () in
+    List.iter (function i -> printModule (Names.id_of_string i) None) ml ;
+    verbose := oldverbose
+;;
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
diff --git a/contrib/xml/xmlentries.ml b/contrib/xml/xmlentries.ml
new file mode 100644
index 0000000000..2376bd0194
--- /dev/null
+++ b/contrib/xml/xmlentries.ml
@@ -0,0 +1,44 @@
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                     A tactic to print Coq objects in XML                   *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 18/10/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_IDENTIFIER id] ->
+        (fun () -> Xmlcommand.print id None)
+   | [VARG_IDENTIFIER 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_IDENTIFIER id] -> (fun () -> Xmlcommand.printModule id None)
+   | [VARG_IDENTIFIER id ; VARG_STRING dn] ->
+        (fun () -> Xmlcommand.printModule id (Some dn))
+   | _  -> anomaly "This should be trapped");;