X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcic2Xml.ml;fp=helm%2FgTopLevel%2Fcic2Xml.ml;h=b4b1f239ab888476836dd298c0769c94c4c25b93;hb=34320b90dd8eff0a3e14e2f15b8e3de59c49b9b4;hp=6bef2dd439c6ebe5f223649c9f9f101644357745;hpb=c313e16a5cc51ef7c4766aaafdf8f681eaf3d762;p=helm.git diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml index 6bef2dd43..b4b1f239a 100644 --- a/helm/gTopLevel/cic2Xml.ml +++ b/helm/gTopLevel/cic2Xml.ml @@ -89,7 +89,7 @@ let print_term ~ids_to_inner_sorts = X.xml_nempty "PROD" ["type",sort] [< List.fold_left (fun i (id,binder,s) -> - let sort = Hashtbl.find ids_to_inner_sorts id in + let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in let attrs = ("id",id)::("type",sort):: match binder with @@ -120,7 +120,6 @@ let print_term ~ids_to_inner_sorts = [< List.fold_left (fun i (id,binder,s) -> let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in - let _ = prerr_endline ("AHHHHHHHHHHHHHHHHH" ^ sort) in let attrs = ("id",id)::("type",sort):: match binder with