Report des modifs de Claudio

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

4 files changed, 24 insertions, 20 deletions

diff --git a/contrib/xml/Xml.v b/contrib/xml/Xml.v
index f1d91371e..91fe6295a 100644
--- a/contrib/xml/Xml.v
+++ b/contrib/xml/Xml.v
@@ -33,10 +33,10 @@ Grammar vernac vernac : ast :=
 | xml_print_all [ "Print" "XML" "All" "." ] ->
                [(XmlPrintAll)]
 
-| xml_print_module [ "Print" "XML" "Module" identarg($id) "." ] ->
+| xml_print_module [ "Print" "XML" "Module" tactic:qualidarg($id) "." ] ->
                [(XmlPrintModule $id)]
 
-| xml_print_module_disk [ "Print" "XML" "Module" "Disk" stringarg($dn) identarg($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) "." ] ->
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 6e7548596..3116bd49b 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -268,10 +268,10 @@ let print_term inner_types l env csr =
    let type_of_term =
     Reduction.nf_betaiota (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 -> InnerProp type_of_term
-     | T.Prop _      -> InnerSet
-     | _             -> InnerType
+    match R.get_sort_family_of env (Evd.empty) type_of_term with
+       T.InProp -> InnerProp type_of_term
+     | T.InSet  -> InnerSet
+     | T.InType -> InnerType
   in
 
 (*WHICH FORCE FUNCTION DEPENDS ON THE ORDERING YOU WANT
@@ -879,7 +879,7 @@ let print_object lobj id sp dn fv env =
 let rec print_library_segment state bprintleaf dn =
   List.iter
    (function (sp, node) ->
-     print_if_verbose (Names.string_of_path sp ^ "\n") ;
+     print_if_verbose ("Print_library_segment: " ^ Names.string_of_path sp ^ "\n") ;
      print_node node (Names.basename sp) sp bprintleaf dn ;
      print_if_verbose "\n"
    ) (List.rev state)
@@ -895,6 +895,7 @@ and print_node n id sp bprintleaf dn =
          if not (List.mem id !printed) then
           (* this is an uncooked term or a local (with no namesakes) term *)
           begin
+try
            if could_have_namesakes o sp then
             begin
              (* this is an uncooked term *)
@@ -908,6 +909,7 @@ and print_node n id sp bprintleaf dn =
              print_if_verbose ("OK, stampo " ^ Names.string_of_id id ^ "\n") ;
              print_object o id sp dn !pvars !cumenv
             end
+with _ -> print_if_verbose ("EXCEPTION RAISED!!!\n");
           end
          else
           begin
@@ -959,18 +961,20 @@ let print_closed_section s ls dn =
 (* 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 printModule qid dn =
  let module L = Library in
- let module N = Names in
+ let module N = Nametab 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 [id]) in
-   print_if_verbose ("MODULE_BEGIN " ^ str ^ " " ^ N.string_of_path sp ^ " " ^
-    (L.module_full_filename [id]) ^ "\n") ;
+
+  let (_,dir_path,_) = L.locate_qualified_library qid in
+
+  let str = N.string_of_qualid qid in 
+  let ls = L.module_segment (Some dir_path) in
+   print_if_verbose ("MODULE_BEGIN " ^ str ^ " " ^
+    (L.module_full_filename dir_path) ^ "\n") ;
    print_closed_section str (List.rev ls) dn ;
-   print_if_verbose ("MODULE_END " ^ str ^ " " ^ N.string_of_path sp ^ " " ^
-    (L.module_full_filename [id]) ^ "\n")
+   print_if_verbose ("MODULE_END " ^ str ^ " " ^
+    (L.module_full_filename dir_path) ^ "\n")
 ;;
 
 (* printSection identifier directory_name                                    *)
diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli
index 0ddc01c9a..6d8250ef7 100644
--- a/contrib/xml/xmlcommand.mli
+++ b/contrib/xml/xmlcommand.mli
@@ -40,13 +40,13 @@ val show : string option -> unit
 val printAll : unit -> unit
 
 (* printModule identifier directory_name *)
-(*  where identifier     is the name of a module d                           *)
+(*  where identifier     is the qualified 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
+val printModule : Nametab.qualid -> string option -> unit
 
 (* printSection identifier directory_name *)
 (*  where identifier     is the name of a closed section d                   *)
diff --git a/contrib/xml/xmlentries.ml b/contrib/xml/xmlentries.ml
index 093727f2f..2323adaa0 100644
--- a/contrib/xml/xmlentries.ml
+++ b/contrib/xml/xmlentries.ml
@@ -45,8 +45,8 @@ vinterp_add "XmlPrintAll"
 
 vinterp_add "XmlPrintModule"
  (function
-     [VARG_IDENTIFIER id] -> (fun () -> Xmlcommand.printModule id None)
-   | [VARG_IDENTIFIER id ; VARG_STRING dn] ->
+     [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");;