X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_annotations%2FcicXPath.ml;h=75a598d91990728b4361452e750bc7669778cd6c;hb=0c6a5aadb1a7746681a8e26fc0b009f847c10557;hp=1eaf31f4e97611319a3e8759c7297a51e014104f;hpb=ae326f646ef4c01b43d6da04201b427d1e175400;p=helm.git

diff --git a/helm/ocaml/cic_annotations/cicXPath.ml b/helm/ocaml/cic_annotations/cicXPath.ml
index 1eaf31f4e..75a598d91 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
@@ -54,11 +56,10 @@ let get_ids_to_targets annobj =
    in
     let rec add_target_term t =
      match t with
-        C.ARel (id,_,_)
-      | C.AVar (id,_)
-      | C.AMeta (id,_)
+        C.ARel (id,_,_,_)
+      | C.AMeta (id,_,_)
       | C.ASort (id,_)
-      | C.AImplicit id ->
+      | C.AImplicit (id, _) ->
          set_target id (C.Term t)
       | C.ACast (id,va,ty) ->
          set_target id (C.Term t) ;
@@ -73,56 +74,71 @@ let get_ids_to_targets annobj =
       | C.AAppl (id,l) ->
          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)
-      | C.AMutCase (id,_,_,_,ot,it,pl) ->
+      | C.AVar (id,_,exp_named_subst)
+      | C.AConst (id,_,exp_named_subst)
+      | C.AMutInd (id,_,_,exp_named_subst)
+      | C.AMutConstruct (id,_,_,_,exp_named_subst) ->
+         set_target id (C.Term t) ;
+         List.iter (function (_,t) -> add_target_term t) exp_named_subst
+      | C.AMutCase (id,_,_,ot,it,pl) ->
          set_target id (C.Term t) ;
          List.iter add_target_term (ot::it::pl)
       | C.AFix (id,_,ifl) ->
          set_target id (C.Term t) ;
          List.iter
-          (function (_,_,ty,bo) ->
+          (function (_,_,_,ty,bo) ->
             add_target_term ty ;
             add_target_term bo
           ) ifl
       | C.ACoFix (id,_,cfl) ->
          set_target id (C.Term t) ;
          List.iter
-          (function (_,ty,bo) ->
+          (function (_,_,ty,bo) ->
             add_target_term ty ;
             add_target_term bo
           ) cfl
     in
      let add_target_obj annobj =
       match annobj with
-        C.ADefinition (id,_,bo,ty,_) ->
-         set_target id (C.Object annobj) ;
-         add_target_term bo ;
-         add_target_term ty
-      | C.AAxiom (id,_,ty,_) ->
+        C.AConstant (id,idbody,_,bo,ty,_) ->
          set_target id (C.Object annobj) ;
+         (match idbody,bo with
+             Some idbody,Some bo ->
+              set_target idbody (C.ConstantBody annobj) ;
+              add_target_term bo
+           | None, None -> ()
+           | _,_ -> assert false
+         ) ;
          add_target_term ty
-      | C.AVariable (id,_,None,ty) ->
+      | C.AVariable (id,_,None,ty,_) ->
          set_target id (C.Object annobj) ;
          add_target_term ty
-      | C.AVariable (id,_,Some bo,ty) ->
+      | C.AVariable (id,_,Some bo,ty,_) ->
          set_target id (C.Object annobj) ;
          add_target_term bo ;
          add_target_term ty
-      | C.ACurrentProof (id,_,cl,bo,ty) ->
+      | C.ACurrentProof (id,idbody,_,cl,bo,ty,_) ->
          set_target id (C.Object annobj) ;
-         List.iter (function (_,t) -> add_target_term t) cl ;
+         set_target idbody (C.ConstantBody annobj) ;
+         List.iter (function (cid,_,context, t) as annconj ->
+           set_target cid (C.Conjecture annconj) ;
+	   List.iter 
+	     (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
       | C.AInductiveDefinition (id,itl,_,_) ->
          set_target id (C.Object annobj) ;
          List.iter
-          (function (_,_,arity,cl) ->
+          (function (_,_,_,arity,cl) ->
             add_target_term arity ;
-            List.iter (function (_,ty,_) -> add_target_term ty) cl
+            List.iter (function (_,ty) -> add_target_term ty) cl
           ) itl
      in
       add_target_obj annobj ;