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

diff --git a/helm/ocaml/cic_annotations/cicXPath.ml b/helm/ocaml/cic_annotations/cicXPath.ml
index 76cb7f75a..f2cb0ed40 100644
--- a/helm/ocaml/cic_annotations/cicXPath.ml
+++ b/helm/ocaml/cic_annotations/cicXPath.ml
@@ -76,7 +76,6 @@ let get_ids_to_targets annobj =
          set_target id (C.Term t) ;
          List.iter add_target_term l
       | C.AConst (id,_,_)
-      | C.AAbst (id,_)
       | C.AMutInd (id,_,_,_)
       | C.AMutConstruct (id,_,_,_,_) ->
          set_target id (C.Term t)
@@ -116,13 +115,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