* Abst removed from the DTD

[helm.git] / helm / gTopLevel / cic2Xml.ml

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index ad1d1f8818fb244190075feb9b0223e5db4c77ad..e6a03a645163278770a32feba4c75aa4d2fb6765 100644 (file)
--- a/helm/gTopLevel/cic2Xml.ml
+++ b/helm/gTopLevel/cic2Xml.ml
@@ -116,7 +116,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) ;
@@ -236,13 +235,18 @@ let print_object curi ids_to_inner_sorts =
 ;;
 
 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 [<>]
    )