X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_annotations%2FcicAnnotation2Xml.ml;h=4c028208f05043a12d43b12081b3b02efb9b453f;hb=de9a83f286eee12117fb478ea2db18f7faebac9a;hp=23c3a9b68446a3812f8682a7c2a0e96c78051ac4;hpb=6f65a2e518d723ea722b23bfd9fa0162ff8be457;p=helm.git

diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
index 23c3a9b68..4c028208f 100644
--- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
+++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
@@ -109,7 +109,7 @@ let pp_annotation obj i2a curi =
       [None, "of", UriManager.string_of_uri (UriManager.cicuri_of_uri curi)]
       begin
        match obj with
-         C.AConstant (xid, xidobj, _, te, ty, _) ->
+         C.AConstant (xid, xidobj, _, te, ty, _, _) ->
           [< print_ann i2a xid ;
              (match xidobj,te with
                  Some xidobj, Some te ->
@@ -121,7 +121,7 @@ let pp_annotation obj i2a curi =
              ) ;
              print_term i2a ty
           >]
-       | C.AVariable (xid, _, bo, ty,_) ->
+       | C.AVariable (xid, _, bo, ty,_, _) ->
           [< print_ann i2a xid ;
              (match bo with
                  None -> [<>]
@@ -129,7 +129,7 @@ let pp_annotation obj i2a curi =
              ) ;
              print_term i2a ty
           >]
-       | C.ACurrentProof (xid, xidobj, _, conjs, bo, ty,_) ->
+       | C.ACurrentProof (xid, xidobj, _, conjs, bo, ty,_, _) ->
           [< print_ann i2a xid ;
              print_ann i2a xidobj ;
              List.fold_right
@@ -151,7 +151,7 @@ let pp_annotation obj i2a curi =
              print_term i2a bo ;
              print_term i2a ty
           >]
-       | C.AInductiveDefinition (xid, tys, params, paramsno) ->
+       | C.AInductiveDefinition (xid, tys, params, paramsno, _) ->
           [< print_ann i2a xid ;
              List.fold_right
               (fun x i -> [< print_mutual_inductive_type i2a x ; i >])