X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_annotations%2FcicAnnotation2Xml.ml;h=1961a2bc2c726ddd7c920729bd2998e6d7ea003d;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=8fb002f3f0d87286dd7a182fa215276ceee8a1cd;hpb=37f08b2aba9f17d9d609ca0f57d607f437a3d3fc;p=helm.git

diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
index 8fb002f3f..1961a2bc2 100644
--- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
+++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
@@ -64,7 +64,6 @@ let print_term i2a =
            List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]
         >]
      | C.AConst (id,_,_) -> print_ann i2a id
-     | C.AAbst (id,_) -> raise NotImplemented
      | C.AMutInd (id,_,_,_) -> print_ann i2a id
      | C.AMutConstruct (id,_,_,_,_) -> print_ann i2a id
      | C.AMutCase (id,_,_,_,ty,te,patterns) ->
@@ -119,10 +118,12 @@ let pp_annotation obj i2a curi =
        | C.ACurrentProof (xid, _, conjs, bo, ty) ->
           [< print_ann i2a xid ;
              List.fold_right
-              (fun (_, context, t) i ->
-                [< List.fold_right
-		    (fun context_entry i -> 
-		      [<(match context_entry with
+              (fun (cid, _, context, t) i ->
+                [< print_ann i2a cid ;
+                   List.fold_right
+		    (fun (hid,context_entry) i -> 
+		      [<print_ann i2a hid ;
+                        (match context_entry with
 			    Some (_,C.ADecl at) -> print_term i2a at
 		          | Some (_,C.ADef at) -> print_term i2a at
 		          | None -> [< >]