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

diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
index 8d12434cb..8fb002f3f 100644
--- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
+++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
@@ -42,6 +42,8 @@ let print_ann i2a id =
 ;;
 
 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
+(* It takes in input a hash table mapping ids to annotations, an annotated 
+term, and gives back a Xml.token Stream.t representing the .ann file *)
 let print_term i2a =
  let rec aux =
   let module C = Cic in
@@ -50,7 +52,7 @@ let print_term i2a =
     function
        C.ARel (id,_,_) -> print_ann i2a id
      | C.AVar (id,_) -> print_ann i2a id
-     | C.AMeta (id,_) -> print_ann i2a id
+     | C.AMeta (id,_,_) -> print_ann i2a id
      | C.ASort (id,_) -> print_ann i2a id
      | C.AImplicit _ -> raise NotImplemented
      | C.AProd (id,_,s,t) -> [< print_ann i2a id ; aux s ; aux t >]
@@ -117,8 +119,19 @@ let pp_annotation obj i2a curi =
        | C.ACurrentProof (xid, _, conjs, bo, ty) ->
           [< print_ann i2a xid ;
              List.fold_right
-              (fun (_,t) i -> [< print_term i2a t ; i >])
-              conjs [<>] ;
+              (fun (_, context, t) i ->
+                [< List.fold_right
+		    (fun context_entry i -> 
+		      [<(match context_entry with
+			    Some (_,C.ADecl at) -> print_term i2a at
+		          | Some (_,C.ADef at) -> print_term i2a at
+		          | None -> [< >]
+                        ) ; i
+                       >]
+		    ) context [< >];
+		   print_term i2a t ; i
+                >]
+              ) conjs [<>] ;
              print_term i2a bo ;
              print_term i2a ty
           >]
@@ -131,3 +144,6 @@ let pp_annotation obj i2a curi =
       end
   >]
 ;;
+
+
+