Conjectures and Hypotheses inside every conjecture and in the sequents now

[helm.git] / helm / ocaml / cic_annotations / cicAnnotation2Xml.ml

diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
index 8fb002f3f0d87286dd7a182fa215276ceee8a1cd..7ea0b7b6309937574d1cae19e93d9345928aed46 100644 (file)
--- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
+++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
@@ -119,10 +119,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 -> [< >]