X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2Fcic2Xml.ml;h=0708a839f49439ddb424e5201f2ce75272b44198;hb=HEAD;hp=eb3b93408255d76f677a48948b0aa44762e6e53a;hpb=81cb773cbc402fc74752fb69a436b25be49489ee;p=helm.git

diff --git a/helm/software/components/cic_acic/cic2Xml.ml b/helm/software/components/cic_acic/cic2Xml.ml
index eb3b93408..0708a839f 100644
--- a/helm/software/components/cic_acic/cic2Xml.ml
+++ b/helm/software/components/cic_acic/cic2Xml.ml
@@ -137,21 +137,21 @@ let print_term ?ids_to_inner_sorts =
                 ) [< >] lambdas ;
                X.xml_nempty "target" [] (aux t)
             >]
-     | C.ALetIn (xid,C.Anonymous,s,t) ->
+     | C.ALetIn (xid,C.Anonymous,s,ty,t) ->
        assert false
-     | C.ALetIn (last_id,C.Name _,_,_) as letins ->
+     | C.ALetIn (last_id,C.Name _,_,_,_) as letins ->
         let rec eat_letins =
          function
-            C.ALetIn (id,n,s,t) ->
+            C.ALetIn (id,n,s,ty,t) ->
              let letins,t' = eat_letins t in
-              (id,n,s)::letins,t'
+              (id,n,s,ty)::letins,t'
           | t -> [],t
         in
          let letins,t = eat_letins letins in
           let sort = find_sort "sort" last_id in
            X.xml_nempty "LETIN" sort
             [< List.fold_left
-                (fun i (id,binder,s) ->
+                (fun i (id,binder,s,ty) ->
                   let sort = find_sort "sort" id in
                    let attrs =
                     sort @ ((None,"id",id)::
@@ -159,7 +159,7 @@ let print_term ?ids_to_inner_sorts =
                         C.Anonymous -> []
                       | C.Name b -> [None,"binder",b])
                    in
-                    [< i ; X.xml_nempty "def" attrs (aux s) >]
+                    [< i ; X.xml_nempty "def" attrs [< aux s ; aux ty >] >]
                 ) [< >] letins ;
                X.xml_nempty "target" [] (aux t)
             >]
@@ -345,7 +345,7 @@ let print_object uri
                                         [None,"id",hid;None,"name",n']
                                      | C.Anonymous -> [None,"id",hid])
                                    (print_term ?ids_to_inner_sorts t)
-                               | Some (n,C.ADef t) ->
+                               | Some (n,C.ADef (t,_)) ->
                                   X.xml_nempty "Def"
                                    (match n with
                                        C.Name n' ->