Porting from V6 finished, but not working.

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

2 files changed, 26 insertions, 27 deletions

diff --git a/contrib/xml/cooking.ml b/contrib/xml/cooking.ml
index 19420ff46..10c8d80ef 100644
--- a/contrib/xml/cooking.ml
+++ b/contrib/xml/cooking.ml
@@ -57,32 +57,31 @@ let get_params_from_type vl t =
  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 add_cooking_information sp vl =
+ let module D = Declarations in
+ let module G = Global 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"
-*) ""
+ let module T = Term in
+ let module X = Xml in
+  try
+   let {D.const_body=val0 ; D.const_type = typ} = G.lookup_constant sp in
+   let typ = T.body_of_type typ in
+    get_params_from_type vl typ
+  with
+   Not_found ->
+    try
+     let {D.mind_packets=packs ; D.mind_nparams=nparams} =
+      G.lookup_mind sp
+     in
+      let {D.mind_nf_arity=arity} = packs.(0) in
+      let arity = T.body_of_type arity in
+       get_params_from_type vl arity
+    with
+     Not_found -> Util.anomaly "Cooking of an uncoockable term required"
 ;;
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 1206892cf..6364d258c 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -15,7 +15,7 @@
 (* CONFIGURATION PARAMETERS *)
 
 let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
-let verbose = ref false;; (* always set to true during a "Print XML All" *)
+let verbose = ref true;; (* always set to true during a "Print XML All" *)
 
 
 
@@ -62,7 +62,7 @@ let print_if_verbose s = if !verbose then print_string s;;
 let ext_of_tag =
  function
     "CONSTANT"        -> "con"
-  | "MUTUALINDUCTIVE" -> "ind"
+  | "INDUCTIVE"       -> "ind"
   | "VARIABLE"        -> "var"
   | _                 -> "err" (* uninteresting thing that won't be printed *)
 ;;
@@ -75,7 +75,7 @@ let tag_of_sp sp =
   with
    Not_found ->
     try
-     let _ = G.lookup_mind sp in "MUTUALINDUCTIVE"
+     let _ = G.lookup_mind sp in "INDUCTIVE"
     with
      Not_found ->
       (* We could only hope it is a variable *)
@@ -88,6 +88,7 @@ let tag_of_sp sp =
 let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
  let module D = Declare in
   let tag = Libobject.object_tag o in
+   print_if_verbose ("Object tag: " ^ tag ^ "\n") ;
    match tag with
       "CONSTANT" ->
         (match D.constant_strength sp with
@@ -95,7 +96,7 @@ let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
           | D.NeverDischarge -> true  (* a non-local one    *)
         )
     | "VARIABLE"        -> false  (* variables are local, so no namesakes     *)
-    | "MUTUALINDUCTIVE" -> true   (* mutual inductive types are never local   *)
+    | "INDUCTIVE"       -> true   (* mutual inductive types are never local   *)
     | _                 -> false  (* uninteresting thing that won't be printed*)
 ;;
 
@@ -622,14 +623,13 @@ let print_object o id sp dn fv =
                   D.Cooked c -> print_definition id c typ fv
                 | D.Recipe _ -> Util.anomaly "trying to print a recipe"
           end
-    | "MUTUALINDUCTIVE" ->
+    | "INDUCTIVE" ->
          (*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)