* added mysterious function (Claudio can detail on it)

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

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index df460edce8c6fd5bdb42893cae0342818569fbbe..b4b1f239ab888476836dd298c0769c94c4c25b93 100644 (file)
--- 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
@@ -119,7 +119,7 @@ let print_term ~ids_to_inner_sorts =
            X.xml_nempty "LAMBDA" ["sort",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