- changed license to lgpl

[helm.git] / helm / ocaml / cic_annotations / cicXPath.ml

diff --git a/helm/ocaml/cic_annotations/cicXPath.ml b/helm/ocaml/cic_annotations/cicXPath.ml
index 75a598d91990728b4361452e750bc7669778cd6c..b9533d18f8a46ef77afca96a4196962c7ba8c672 100644 (file)
--- 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) ->