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

diff --git a/helm/ocaml/cic_annotations/cicXPath.ml b/helm/ocaml/cic_annotations/cicXPath.ml
index 1eaf31f4e..76cb7f75a 100644
--- a/helm/ocaml/cic_annotations/cicXPath.ml
+++ b/helm/ocaml/cic_annotations/cicXPath.ml
@@ -42,6 +42,8 @@ let get_annotation ids_to_annotations xpath =
 
 exception MoreThanOneTargetFor of Cic.id;;
 
+(* creates a hashtable mapping each unique id to a node of the annotated 
+object *)
 let get_ids_to_targets annobj =
  let module C = Cic in
   let ids_to_targets = Hashtbl.create 503 in
@@ -56,7 +58,7 @@ let get_ids_to_targets annobj =
      match t with
         C.ARel (id,_,_)
       | C.AVar (id,_)
-      | C.AMeta (id,_)
+      | C.AMeta (id,_,_)
       | C.ASort (id,_)
       | C.AImplicit id ->
          set_target id (C.Term t)
@@ -114,7 +116,14 @@ 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 (_,t) -> add_target_term t) cl ;
+         List.iter (function (_,context, t) -> 
+	   List.iter 
+	     (function 
+		 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
       | C.AInductiveDefinition (id,itl,_,_) ->