Many improvements. Xml contrib retached to the V7.

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

4 files changed, 265 insertions, 209 deletions

diff --git a/contrib/xml/Xml.v b/contrib/xml/Xml.v
index edd50e79d..5753363bd 100644
--- a/contrib/xml/Xml.v
+++ b/contrib/xml/Xml.v
@@ -11,7 +11,7 @@
 Declare ML Module "xml" "xmlcommand" "xmlentries".
 
 Grammar vernac vernac : ast :=
-  xml_print [ "Print" "XML" identarg($id) "." ] ->
+  xml_print [ "Print" "XML" tactic:qualidarg($id) "." ] ->
                [(Print $id)]
 
 | xml_print_file [ "Print" "XML" "File" stringarg($fn) identarg($id) "." ] ->
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 926d35057..df79fe3f7 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -21,28 +21,29 @@ let verbose = ref true;; (* always set to true during a "Print XML All" *)
 
 let print_if_verbose s = if !verbose then print_string s;;
 
-let ext_of_tag =
+type tag =
+   Constant
+ | Inductive
+ | Variable
+;;
+
+(* Next exception is used only inside print_object and tag_of_string_tag *)
+exception Uninteresting;;
+
+let tag_of_string_tag =
  function
     "CONSTANT"
-  | "PARAMETER"       -> "con"
-  | "INDUCTIVE"       -> "ind"
-  | "VARIABLE"        -> "var"
-  | _                 -> "err" (* uninteresting thing that won't be printed *)
+  | "PARAMETER"       -> Constant
+  | "INDUCTIVE"       -> Inductive
+  | "VARIABLE"        -> Variable
+  | _                 -> raise Uninteresting
 ;;
 
-(*CSC: ORRENDO!!! MODIFICARE V7*)
-let tag_of_sp sp =
- let module G = Global in
-  try
-   let _ = G.lookup_constant sp in "CONSTANT" (*V7 Non distinguo gli assiomi*)
-  with
-   Not_found ->
-    try
-     let _ = G.lookup_mind sp in "INDUCTIVE"
-    with
-     Not_found ->
-      (* We could only hope it is a variable *)
-      "VARIABLE"
+let ext_of_tag =
+ function
+    Constant  -> "con"
+  | Inductive -> "ind"
+  | Variable  -> "var"
 ;;
 
 (* could_have_namesakes sp = true iff o is an object that could be cooked and *)
@@ -105,9 +106,9 @@ let trim_wrong_uri_prefix pref {System.relative_subdir=rs ; System.directory=d}
 
 (* uri_of_path sp is a broken (wrong) uri pointing to the object whose        *)
 (* section path is sp                                                         *)
-let uri_of_path sp =
+let uri_of_path sp tag =
  let module N = Names in
-  let ext_of_sp sp = ext_of_tag (tag_of_sp sp) in
+  let ext_of_sp sp = ext_of_tag tag in
    let (sl,id,_) = N.repr_path sp in
     let module_path =
      match sl with
@@ -141,7 +142,8 @@ let string_of_name =
 
 (*CSC: commento sbagliato ed obsoleto *)
 (* list of variables availables in the actual section *)
-let pvars = ref [];;
+let pvars = ref ([[]] : string list list);;
+let cumenv = ref Environ.empty_env;;
 
 let string_of_vars_list =
  let add_prefix n s = string_of_int n ^ ": " ^ s in
@@ -179,13 +181,15 @@ let string_of_pvars pvars hyps =
   let rec aux n =
    function
       [] -> assert false
-(*print_string "\nPVARS:" ;
+(* (-1,"?") For Print XML *)
+(*
+print_string "\nPVARS:" ;
 List.iter (List.iter print_string) pvars ;
 print_string "\nHYPS:" ;
 List.iter print_string hyps ;
 print_string "\n" ;
 flush stdout ;
-(-1,"?")
+assert false
 *)
     | l::_ when List.mem v l -> (n,v)
     | _::tl -> aux (n+1) tl
@@ -195,12 +199,25 @@ flush stdout ;
   string_of_vars_list (List.map (find_depth pvars) (List.rev hyps))
 ;;
 
-exception XmlCommandInternalError;;
+type variables_type = 
+   Definition of string * Term.constr * Term.types
+ | Assumption of string * Term.constr
+;;
 
-let add_to_pvars v =
- match !pvars with
-    []       -> raise XmlCommandInternalError
-  | (he::tl) -> pvars := (v::he)::tl
+let add_to_pvars x =
+ let module E = Environ in
+  let v =
+   match x with
+      Definition (v, bod, typ) ->
+       cumenv := E.push_named_def (Names.id_of_string v, bod, typ) !cumenv ;
+       v
+    | Assumption (v, typ) ->
+       cumenv := E.push_named_assum (Names.id_of_string v, typ) !cumenv ;
+       v
+  in
+   match !pvars with
+      []       -> assert false
+    | (he::tl) -> pvars := (v::he)::tl
 ;;
 
 let get_depth_of_var v =
@@ -232,21 +249,32 @@ let get_next_id () =
 ;;
 
 (* 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 print_term inner_types l env csr =
  let module N = Names in
+ let module E = Environ in
  let module T = Term in
  let module X = Xml in
+ let module R = Retyping 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 =
+
+  let rec inner_type_display l env term =
+   let type_of_term = R.get_type_of env (Evd.empty) term in
+   match R.get_sort_of env (Evd.empty) type_of_term with
+      T.Prop (T.Null) -> Some (term_display l env type_of_term)
+    | _               -> None
+
+  and term_display l env cstr =
+   let xmlinnertype = inner_type_display l env cstr in
+   let next_id = get_next_id () in
+    inner_types := (next_id, xmlinnertype)::!inner_types ;
    (* 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
@@ -256,8 +284,10 @@ let print_term l csr =
             X.xml_empty "REL"
              ["value",(string_of_int n) ;
               "binder",(N.string_of_id id) ;
-              "id", get_next_id ()]
-        | N.Anonymous -> raise XmlCommandInternalError
+              "id", next_id]
+        | N.Anonymous ->
+(*V7Local assert false*)
+X.xml_empty "REL" ["binder","BUG"]
      )
    | T.IsVar id ->
       let depth =
@@ -268,83 +298,112 @@ let print_term l csr =
       in
        X.xml_empty "VAR"
         ["relUri",depth ^ "," ^ (N.string_of_id id) ;
-         "id", get_next_id ()]
+         "id", next_id]
    | T.IsMeta n ->
-      X.xml_empty "META" ["no",(string_of_int n) ; "id", get_next_id ()]
+      X.xml_empty "META" ["no",(string_of_int n) ; "id", next_id]
    | T.IsSort s ->
-      X.xml_empty "SORT" ["value",(string_of_sort s) ; "id", get_next_id ()]
+      X.xml_empty "SORT" ["value",(string_of_sort s) ; "id", 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)
+      X.xml_nempty "CAST" ["id", next_id]
+       [< X.xml_nempty "term" [] (term_display l env t1) ;
+          X.xml_nempty "type" [] (term_display l env t2)
        >]
-   | T.IsLetIn (nid,s,_,d)->
+   | T.IsLetIn (nid,s,t,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 "LETIN" ["id", next_id]
+        [< X.xml_nempty "term" [] (term_display l env s) ;
            X.xml_nempty "target" ["binder",(N.string_of_id nid')]
-            (term_display ((N.Name nid')::l) d)
+            (term_display
+             ((N.Name nid')::l)
+             (E.push_rel_def (N.Name nid', s, t) env)
+             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 "PROD" ["id", next_id]
+        [< X.xml_nempty "source" [] (term_display l env t1) ;
            X.xml_nempty "target" ["binder",(N.string_of_id nid')]
-            (term_display ((N.Name nid')::l) t2)
+            (term_display
+             ((N.Name nid')::l)
+             (E.push_rel_assum (N.Name nid', t1) env)
+             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)
+      X.xml_nempty "PROD" ["id", next_id]
+       [< X.xml_nempty "source" [] (term_display l env t1) ;
+          X.xml_nempty "target" []
+           (term_display
+            (nid::l)
+            (E.push_rel_assum (nid, t1) env)
+            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 "LAMBDA" ["id", next_id]
+        [< X.xml_nempty "source" [] (term_display l env t1) ;
            X.xml_nempty "target" ["binder",(N.string_of_id nid')]
-            (term_display ((N.Name nid')::l) t2)
+            (term_display
+             ((N.Name nid')::l)
+             (E.push_rel_assum (N.Name nid', t1) env)
+             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) >]
+      X.xml_nempty "LAMBDA" ["id", next_id]
+       [< X.xml_nempty "source" [] (term_display l env t1) ;
+          X.xml_nempty "target" []
+           (term_display
+            (nid::l)
+            (E.push_rel_assum (nid, t1) env)
+            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 [<>])
+      X.xml_nempty "APPLY" ["id", next_id]
+       [< (term_display l env h) ;
+          (Array.fold_right (fun x i -> [< (term_display l env x); i >]) t [<>])
        >]
    | T.IsConst (sp,_) ->
-      X.xml_empty "CONST" ["uri",(uri_of_path sp) ; "id", get_next_id ()]
+      X.xml_empty "CONST"
+       ["uri",(uri_of_path sp Constant) ; "id", next_id]
    | T.IsMutInd ((sp,i),_) ->
       X.xml_empty "MUTIND"
-       ["uri",(uri_of_path sp) ;
+       ["uri",(uri_of_path sp Inductive) ;
         "noType",(string_of_int i) ;
-        "id", get_next_id ()]
+        "id", next_id]
    | T.IsMutConstruct (((sp,i),j),_) ->
       X.xml_empty "MUTCONSTRUCT"
-       ["uri",(uri_of_path sp) ;
+       ["uri",(uri_of_path sp Inductive) ;
         "noType",(string_of_int i) ;
         "noConstr",(string_of_int j) ;
-        "id", get_next_id ()]
+        "id", next_id]
    | T.IsMutCase ((_,((sp,i),_,_,_,_)),ty,term,a) ->
-      let (uri, typeno) = (uri_of_path sp),i in
+      let (uri, typeno) = (uri_of_path sp Inductive),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) >] ;
+        ["uriType",uri ; "noType",(string_of_int typeno) ; "id",next_id]
+        [< X.xml_nempty "patternsType" [] [< (term_display l env ty) >] ;
+	   X.xml_nempty "inductiveTerm" [] [< (term_display l env term) >] ;
 	   Array.fold_right
             (fun x i ->
-              [< X.xml_nempty "pattern" [] [< term_display l x >] ; i>]
+              [< X.xml_nempty "pattern" [] [< term_display l env x >] ; i>]
             ) a [<>]
         >]
-   | T.IsFix ((ai,i),(t,f,b)) ->
-      X.xml_nempty "FIX" ["noFun", (string_of_int i) ; "id",get_next_id ()]
+   | T.IsFix ((ai,i),((t,f,b) as rec_decl)) ->
+      X.xml_nempty "FIX" ["noFun", (string_of_int i) ; "id",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 >]
+	         [< X.xml_nempty "type" [] [< term_display l env ti >] ;
+	            X.xml_nempty "body" [] [<
+                     term_display
+                      ((List.rev f)@l)
+                      (E.push_rec_types rec_decl env)
+                      bi
+                    >]
 	         >] ;
                 i
              >]
@@ -352,13 +411,18 @@ let print_term l csr =
 	   (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 ()]
+   | T.IsCoFix (i,((t,f,b) as rec_decl)) ->
+      X.xml_nempty "COFIX" ["noFun", (string_of_int i) ; "id",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 >]
+	        [< X.xml_nempty "type" [] [< term_display l env ti >] ;
+	           X.xml_nempty "body" [] [<
+                    term_display
+                     ((List.rev f)@l)
+                     (E.push_rec_types rec_decl env)
+                     bi
+                   >]
 	        >] ;
                i
             >]
@@ -372,7 +436,7 @@ let print_term l csr =
   in
     (*CSC: ad l vanno andrebbero aggiunti i nomi da non *)
     (*CSC: mascherare (costanti? variabili?)            *)
-    term_display l csr
+    term_display l env csr
 ;;
 
 (* FUNCTIONS TO PRINT A SINGLE OBJECT OF COQ *)
@@ -386,18 +450,20 @@ let print_term l csr =
 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 >]
-       >]
-  >]
+  let inner_types = ref [] in
+  let env = (Safe_typing.env_of_safe_env (Global.safe_env ())) in
+   [< 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 inner_types [] env t >] ; i >])
+            mv [<>] ;
+           X.xml_nempty "body" [] [< print_term inner_types [] env c >] ;
+           X.xml_nempty "type"  [] [< print_term inner_types [] env typ >]
+        >]
+   >]
 ;;
 
 (* print_axiom id type params                                              *)
@@ -405,18 +471,19 @@ let print_current_proof c typ id mv =
 (*  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 hyps =
+let print_axiom id typ fv hyps env =
  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 () ;
-        "params",(string_of_pvars fv hyps)]
-      [< X.xml_nempty "type" [] (print_term [] typ) >]
-  >]
+  let inner_types = ref [] in
+   [< 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 () ;
+         "params",(string_of_pvars fv hyps)]
+       [< X.xml_nempty "type" [] (print_term inner_types [] env typ) >]
+   >]
 ;;
 
 (* print_definition id term type params hyps                               *)
@@ -425,34 +492,42 @@ let print_axiom id typ fv hyps =
 (*  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 hyps =
+let print_definition id c typ fv hyps env =
  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 () ;
-       "params",(string_of_pvars fv hyps)]
-      [< X.xml_nempty "body" [] (print_term [] c) ;
-         X.xml_nempty "type"  [] (print_term [] typ) >]
-  >]
+  let inner_types = ref [] in
+   [< 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 () ;
+        "params",(string_of_pvars fv hyps)]
+       [< X.xml_nempty "body" [] (print_term inner_types [] env c) ;
+          X.xml_nempty "type"  [] (print_term inner_types [] env 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 print_variable id body typ env =
  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))
-  >]
+  let inner_types = ref [] in
+   [< 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 ()]
+       [< (match body with
+              None -> [<>]
+            | Some body ->
+               X.xml_nempty "body" [] (print_term inner_types [] env body)
+          ) ;
+          X.xml_nempty "type" [] (print_term inner_types [] env typ)
+       >]
+   >]
 ;;
 
 (* print_mutual_inductive_packet p                                           *)
@@ -460,7 +535,7 @@ let print_variable id typ =
 (*          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 print_mutual_inductive_packet inner_types names env p =
  let module D = Declarations in
  let module N = Names in
  let module T = Term in
@@ -476,11 +551,12 @@ let print_mutual_inductive_packet names p =
         "inductive",(string_of_bool finite)
        ]
        [<
-          X.xml_nempty "arity" [] (print_term [] (T.body_of_type arity)) ;
+          X.xml_nempty "arity" []
+           (print_term inner_types [] env (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) ;
+                 (print_term inner_types names env lc) ;
                 i
              >])
 	   (Array.mapi (fun j x -> (x,T.body_of_type lc.(j)) ) consnames )
@@ -497,15 +573,24 @@ let print_mutual_inductive_packet names p =
 (*  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 hyps nparams =
+let print_mutual_inductive packs fv hyps nparams env =
  let module D = Declarations in
+ let module E = Environ in
  let module X = Xml in
  let module N = Names in
+  let inner_types = ref [] in
   let names =
    List.map
     (fun p -> let {D.mind_typename=typename} = p in N.Name(typename))
     (Array.to_list packs)
   in
+  let env =
+   List.fold_right
+    (fun {D.mind_typename=typename ; D.mind_nf_arity=arity} env ->
+     E.push_rel_assum (N.Name typename, arity) env)
+    (Array.to_list packs)
+    env
+  in
    reset_id () ;
    [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
       X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
@@ -515,9 +600,9 @@ let print_mutual_inductive packs fv hyps nparams =
         "id",get_next_id () ;
         "params",(string_of_pvars fv hyps)]
        [< (Array.fold_right
-            (fun x i -> [< print_mutual_inductive_packet names x ; i >])
-            packs
-            [< >]
+            (fun x i ->
+             [< print_mutual_inductive_packet inner_types names env x ; i >]
+            ) packs [< >]
           )
        >]
    >]
@@ -525,56 +610,51 @@ let print_mutual_inductive packs fv hyps nparams =
 
 let string_list_of_named_context_list =
  List.map
-  (function
-      (n,None,_) -> Names.string_of_id n
-    | _          -> assert false
-  )
+  (function (n,_,_) -> Names.string_of_id n)
 ;;
 
 (* print id dest                                                          *)
-(*  where id   is the identifier (name) of a definition/theorem or of an  *)
-(*             inductive definition                                       *)
+(*  where sp   is the qualified identifier (section path) of a            *)
+(*             definition/theorem, variable or 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 print sp 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 (_,str) = N.repr_qualid sp in
+  let id = Names.id_of_string str in
+  let glob_ref = Nametab.locate sp in
+  let env = (Safe_typing.env_of_safe_env (G.safe_env ())) in
   let pp_cmds =
-   begin
-    try
-     let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
-      G.lookup_constant sp in
-     let hyps = string_list_of_named_context_list hyps in
-     let typ = T.body_of_type typ in
-      begin
-       match val0 with
-          None -> print_axiom id typ [] hyps
-        | Some c -> print_definition id c typ [] hyps
-      end
-    with
-     Not_found ->
-      try
+   match glob_ref with
+      T.VarRef sp ->
+       let (body,typ) = G.lookup_named id in
+        print_variable id body (T.body_of_type typ) env
+    | T.ConstRef sp ->
+       let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
+        G.lookup_constant sp in
+       let hyps = string_list_of_named_context_list hyps in
+       let typ = T.body_of_type typ in
+        begin
+         match val0 with
+            None -> print_axiom id typ [] hyps env
+          | Some c -> print_definition id c typ [] hyps env
+        end
+    | T.IndRef (sp,_) ->
        let {D.mind_packets=packs ; D.mind_nparams=nparams ; D.mind_hyps=hyps} =
         G.lookup_mind sp
        in
         let hyps = string_list_of_named_context_list hyps in
-         print_mutual_inductive packs [] hyps nparams
-      with
-       Not_found ->
-        try
-         let (_,typ) = G.lookup_named id in
-          print_variable id (T.body_of_type typ)
-        with
-         Not_found -> Util.anomaly ("print: this should not happen")
-   end
+         print_mutual_inductive packs [] hyps nparams env
+    | T.ConstructRef _
+    | T.EvarRef _ ->
+       Util.anomaly ("print: this should not happen")
   in
    Xml.pp pp_cmds fn
 ;;
@@ -597,7 +677,7 @@ let show fn =
 (*          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 [];;
+let printed = ref [];;
 
 (* makes a filename from a directory name, a section path and an extension *)
 let mkfilename dn sp ext =
@@ -641,9 +721,6 @@ let mkfilename dn sp ext =
         | _ -> assert false
 ;;
 
-(* 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 *)
@@ -656,8 +733,9 @@ exception Uninteresting;;
 (* 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 lobj id sp dn fv =
+let print_object lobj id sp dn fv env =
  let module D = Declarations in
+ let module E = Environ in
  let module G = Global in
  let module N = Names in
  let module T = Term in
@@ -674,8 +752,8 @@ let print_object lobj id sp dn fv =
          let typ = T.body_of_type typ in
           begin
            match val0 with
-              None -> print_axiom id typ fv hyps
-            | Some c -> print_definition id c typ fv hyps
+              None -> print_axiom id typ fv hyps env
+            | Some c -> print_definition id c typ fv hyps env
           end
     | "INDUCTIVE" ->
          let
@@ -685,26 +763,26 @@ let print_object lobj id sp dn fv =
           } = G.lookup_mind sp
          in
           let hyps = string_list_of_named_context_list hyps in
-           print_mutual_inductive packs fv hyps nparams
+           print_mutual_inductive packs fv hyps nparams env
     | "VARIABLE" ->
         let (_,(varentry,_,_)) = Declare.out_variable lobj in
-         add_to_pvars (N.string_of_id id) ;
          begin
           match varentry with
              Declare.SectionLocalDef body ->
-              print_string "************** UNIMPLEMENTED ***********\n" ;
-              flush stdout ;
-              [<>]
+              let typ = Retyping.get_type_of env Evd.empty body in
+               add_to_pvars (Definition (N.string_of_id id, body, typ)) ;
+               print_variable id (Some body) typ env
            | Declare.SectionLocalAssum typ ->
-              print_variable id (T.body_of_type typ)
+              add_to_pvars (Assumption (N.string_of_id id, typ)) ;
+              print_variable id None (T.body_of_type typ) env
          end
     | "CLASS"
     | "COERCION"
     | _ -> raise Uninteresting
-  and fileext = ext_of_tag tag
+  and fileext () = ext_of_tag (tag_of_string_tag tag)
   in
    try
-    Xml.pp (pp_cmds ()) (mkfilename dn sp fileext)
+    Xml.pp (pp_cmds ()) (mkfilename dn sp (fileext ()))
    with
     Uninteresting -> ()
 ;;
@@ -731,44 +809,31 @@ and print_node n id sp bprintleaf dn =
       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
+         if not (List.mem id !printed) then
           (* this is an uncooked term or a local (with no namesakes) term *)
           begin
            if could_have_namesakes o sp then
             begin
              (* this is an uncooked term *)
-             print_if_verbose ("Rimando " ^ Names.string_of_id id ^ "\n") ;
-             toprint := (id,sp,sp,o,!pvars,dn)::!toprint
+             print_if_verbose ("OK, stampo solo questa volta " ^ Names.string_of_id id ^ "\n") ;
+             print_object o id sp dn !pvars !cumenv ;
+             printed := id::!printed
             end
            else
             begin
              (* this is a local term *)
              print_if_verbose ("OK, stampo " ^ Names.string_of_id id ^ "\n") ;
-             print_object o id sp dn !pvars
+             print_object o id sp dn !pvars !cumenv
             end
           end
          else
           begin
            (* update the least cooked sp *)
-           print_if_verbose ("Suppongo gia' stampato " ^ Names.string_of_id id ^ "\n") ;
-           toprint :=
-            List.map
-             (function
-                (id',usp,_,uo,pv,dn) when id' = id -> (id,usp,sp,uo,pv,dn)
-              | t -> t
-             ) !toprint
+           print_if_verbose ("Suppongo gia' stampato " ^ Names.string_of_id id ^ "\n")
           end
        end
-   | L.OpenedSection s -> print_if_verbose ("OpenDir " ^ s ^ "\n")
-   | L.ClosedSection (s,state) ->
+   | L.OpenedSection (s,_) -> print_if_verbose ("OpenDir " ^ s ^ "\n")
+   | L.ClosedSection (_,s,state) ->
       print_if_verbose("ClosedDir " ^ s ^ "\n") ;
       if bprintleaf then
        begin
@@ -777,7 +842,7 @@ and print_node n id sp bprintleaf dn =
         print_library_segment state bprintleaf dn ;
         (* close the scope *)
         match !pvars with
-           [] -> raise XmlCommandInternalError
+           [] -> assert false
          | he::tl -> pvars := tl
        end ;
       print_if_verbose "/ClosedDir\n"
@@ -795,22 +860,11 @@ and print_node n id sp bprintleaf dn =
 (* print_library_segment on all its sons                                     *)
 let print_closed_section s ls dn =
  let module L = Lib in
-  toprint := [] ;
-  (*CSC: this should always be empty yet! But just to be sure... :-) *)
-  pvars := [] ;
+  printed := [] ;
+  pvars := [[]] ;
+  cumenv := Safe_typing.env_of_safe_env (Global.safe_env ()) ;
   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 = pv in
-        pvars := pv ;
-        (*CSC Actual was Some *)
-        print_object uo id usp dn formal_vars
-   ) !toprint ;
   print_if_verbose "\n/Module\n" ;
 ;;
 
@@ -852,7 +906,7 @@ let printSection id dn =
    let rec find_closed_section =
     function
        [] -> raise Not_found
-     | (_,Lib.ClosedSection (str',ls))::_ when str' = str -> ls
+     | (_,Lib.ClosedSection (_,str',ls))::_ when str' = str -> ls
      | _::t -> find_closed_section t
    in
     print_string ("Searching " ^ Names.string_of_path sp ^ "\n") ;
@@ -870,7 +924,9 @@ let printAll () =
   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
index df1a9f8b4..885873bfe 100644
--- a/contrib/xml/xmlcommand.mli
+++ b/contrib/xml/xmlcommand.mli
@@ -19,7 +19,7 @@
 (* 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
+val print : Names.qualid -> string option -> unit
 
 (* show dest                                                  *)
 (*  where dest is either None (for stdout) or (Some filename) *)
diff --git a/contrib/xml/xmlentries.ml b/contrib/xml/xmlentries.ml
index a36d4ae97..e6f792054 100644
--- a/contrib/xml/xmlentries.ml
+++ b/contrib/xml/xmlentries.ml
@@ -17,9 +17,9 @@ open Vernacinterp;;
 
 vinterp_add "Print"
  (function
-     [VARG_IDENTIFIER id] ->
+     [VARG_QUALID id] ->
         (fun () -> Xmlcommand.print id None)
-   | [VARG_IDENTIFIER id ; VARG_STRING fn] ->
+   | [VARG_QUALID id ; VARG_STRING fn] ->
         (fun () -> Xmlcommand.print id (Some fn))
    | _ -> anomaly "This should be trapped");;