Added xml contribution to configure

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

1 files changed, 21 insertions, 11 deletions

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 4440c5063..1206892cf 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -67,6 +67,21 @@ let ext_of_tag =
   | _                 -> "err" (* uninteresting thing that won't be printed *)
 ;;
 
+(*CSC: ORRENDO!!! MODIFICARE V7*)
+let tag_of_sp sp =
+ let module G = Global in
+  try
+   let _ = G.lookup_constant sp in "CONSTANT"
+  with
+   Not_found ->
+    try
+     let _ = G.lookup_mind sp in "MUTUALINDUCTIVE"
+    with
+     Not_found ->
+      (* We could only hope it is a variable *)
+      "VARIABLE"
+;;
+
 (* 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                                              *)
@@ -87,16 +102,7 @@ let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
 (* 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 ext_of_sp sp = ext_of_tag (tag_of_sp sp) in
   let module S = String in
    let str = Names.string_of_path sp in
     let uri = Str.substitute str '#' '/' in
@@ -522,7 +528,11 @@ let print id fn =
         print_mutual_inductive packs (Actual "") nparams
       with
        Not_found ->
-        Util.anomaly ("print: this should not happen")
+        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
   in
    Xml.pp pp_cmds fn