* The interface of CicTypeChecker now allows the usage of definitions in

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

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index db5fd23c57f942e4ec79aaa7f27fb48bd55b6dd0..a25d7f6709ce20cb0bdd17793b3e1a585c46521f 100644 (file)
--- a/helm/gTopLevel/cic2Xml.ml
+++ b/helm/gTopLevel/cic2Xml.ml
@@ -92,7 +92,7 @@ let print_term curi ids_to_inner_sorts =
              X.xml_nempty "target" ["binder",id] (aux t)
           >]
      | C.ALetIn (xid,C.Anonimous,s,t) ->
-       assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*)
+       assert false
      | C.ALetIn (xid,C.Name id,s,t) ->
         let sort = Hashtbl.find ids_to_inner_sorts xid in
          X.xml_nempty "LETIN" ["id",xid ; "sort",sort]
@@ -203,3 +203,16 @@ let print_object curi ids_to_inner_sorts =
  in
   aux
 ;;
+
+let print_inner_types curi ids_to_inner_sorts ids_to_inner_types =
+ let module X = Xml in
+  X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
+   (Hashtbl.fold
+     (fun id ty x ->
+       [< x ;
+          X.xml_nempty "TYPE" ["of",id]
+           (print_term curi ids_to_inner_sorts ty)
+       >]
+     ) ids_to_inner_types [<>]
+   )
+;;