Reindentation.

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

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index f498effb6bc89944c3b068bec8ec69d360d802c0..564493cb83e9d9d2ae42908e3970b21fbb5107be 100644 (file)
--- a/helm/gTopLevel/cic2Xml.ml
+++ b/helm/gTopLevel/cic2Xml.ml
@@ -89,7 +89,9 @@ 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 +121,9 @@ 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
@@ -411,10 +415,11 @@ let
          (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
            [< x ;
               X.xml_nempty "TYPE" ["of",id]
-               [< print_term ids_to_inner_sorts synty ;
-                  match expty with
-                     None -> [<>]
-                   | Some expty' -> print_term ids_to_inner_sorts expty'
+               [< X.xml_nempty "synthesized" []
+                [< print_term ids_to_inner_sorts synty >] ;
+                 match expty with
+                   None -> [<>]
+                 | Some expty' -> X.xml_nempty "expected" [] [< print_term ids_to_inner_sorts expty' >]
                >]
            >]
          ) ids_to_inner_types [<>]