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

diff --git a/helm/ocaml/cic_annotations/cicXPath.ml b/helm/ocaml/cic_annotations/cicXPath.ml
index 75a598d91..b9533d18f 100644
--- a/helm/ocaml/cic_annotations/cicXPath.ml
+++ b/helm/ocaml/cic_annotations/cicXPath.ml
@@ -100,7 +100,7 @@ let get_ids_to_targets annobj =
     in
      let add_target_obj annobj =
       match annobj with
-        C.AConstant (id,idbody,_,bo,ty,_) ->
+        C.AConstant (id,idbody,_,bo,ty,_,_) ->
          set_target id (C.Object annobj) ;
          (match idbody,bo with
              Some idbody,Some bo ->
@@ -110,14 +110,14 @@ let get_ids_to_targets annobj =
            | _,_ -> 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,idbody,_,cl,bo,ty,_) ->
+      | C.ACurrentProof (id,idbody,_,cl,bo,ty,_,_) ->
          set_target id (C.Object annobj) ;
          set_target idbody (C.ConstantBody annobj) ;
          List.iter (function (cid,_,context, t) as annconj ->
@@ -133,7 +133,7 @@ let get_ids_to_targets annobj =
 	   add_target_term t) cl ;
          add_target_term bo ;
          add_target_term ty
-      | C.AInductiveDefinition (id,itl,_,_) ->
+      | C.AInductiveDefinition (id,itl,_,_,_) ->
          set_target id (C.Object annobj) ;
          List.iter
           (function (_,_,_,arity,cl) ->