X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_annotations%2FcicXPath.ml;h=eef9880bcfb6eef4aa6acd674a5a3418735a3078;hb=b57c31a1593872c181249135bc05ebd9a72f523b;hp=76cb7f75ae9167690aa91575a2c6493e69b37382;hpb=82466efd82082c6101d1c2c0c217f681b37160e8;p=helm.git

diff --git a/helm/ocaml/cic_annotations/cicXPath.ml b/helm/ocaml/cic_annotations/cicXPath.ml
index 76cb7f75a..eef9880bc 100644
--- a/helm/ocaml/cic_annotations/cicXPath.ml
+++ b/helm/ocaml/cic_annotations/cicXPath.ml
@@ -116,13 +116,16 @@ let get_ids_to_targets annobj =
          add_target_term ty
       | C.ACurrentProof (id,_,cl,bo,ty) ->
          set_target id (C.Object annobj) ;
-         List.iter (function (_,context, t) -> 
+         List.iter (function (cid,_,context, t) as annconj ->
+           set_target cid (C.Conjecture annconj) ;
 	   List.iter 
-	     (function 
-		 Some (_,C.ADecl at) -> add_target_term at
-	       | Some (_,C.ADef at) -> add_target_term at
-	       | None -> ()
-	     ) context; 
+	     (function ((hid,h) as annhyp) ->
+               set_target hid (C.Hypothesis annhyp) ;
+               match h with
+		  Some (_,C.ADecl at) -> add_target_term at
+	        | Some (_,C.ADef at) -> add_target_term at
+	        | None -> ()
+	     ) context;
 	   add_target_term t) cl ;
          add_target_term bo ;
          add_target_term ty