X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcic2Xml.ml;h=7c674d0ad7eaab5def678e111e89a441e5372933;hb=f41a5585a648d57e4d8a24d664b0a5ce5d591148;hp=ad1d1f8818fb244190075feb9b0223e5db4c77ad;hpb=b57c31a1593872c181249135bc05ebd9a72f523b;p=helm.git

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index ad1d1f881..7c674d0ad 100644
--- a/helm/gTopLevel/cic2Xml.ml
+++ b/helm/gTopLevel/cic2Xml.ml
@@ -1,4 +1,3 @@
-
 (* Copyright (C) 2000, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
@@ -31,7 +30,7 @@ exception NotImplemented;;
 let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
 
 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_term curi ids_to_inner_sorts =
+let print_term curi ~ids_to_inner_sorts =
  let rec aux =
   let module C = Cic in
   let module X = Xml in
@@ -116,7 +115,6 @@ let print_term curi ids_to_inner_sorts =
         let sort = Hashtbl.find ids_to_inner_sorts id in
          X.xml_empty "CONST"
           ["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort]
-     | C.AAbst (id,uri) -> raise NotImplemented
      | C.AMutInd (id,uri,_,i) ->
         X.xml_empty "MUTIND"
          ["uri", (U.string_of_uri uri) ;
@@ -176,7 +174,7 @@ let print_term curi ids_to_inner_sorts =
 exception NotImplemented;;
 
 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_object curi ids_to_inner_sorts =
+let print_object curi ~ids_to_inner_sorts =
  let rec aux =
   let module C = Cic in
   let module X = Xml in
@@ -235,14 +233,19 @@ let print_object curi ids_to_inner_sorts =
   aux
 ;;
 
-let print_inner_types curi ids_to_inner_sorts ids_to_inner_types =
+let print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types =
+ let module C2A = Cic2acic in
  let module X = Xml in
   X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
    (Hashtbl.fold
-     (fun id ty x ->
+     (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
        [< x ;
           X.xml_nempty "TYPE" ["of",id]
-           (print_term curi ids_to_inner_sorts ty)
+           [< print_term curi ids_to_inner_sorts synty ;
+              match expty with
+                 None -> [<>]
+               | Some expty' -> print_term curi ids_to_inner_sorts expty'
+           >]
        >]
      ) ids_to_inner_types [<>]
    )