- the mathql interpreter is not helm-dependent any more

[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 f2cb0ed409e4316155ab5036b0f868bbde9eea32..b20fbd5c03a946f11f7c6e94e7ef5c10c7d5f6f3 100644 (file)
--- a/helm/ocaml/cic_annotations/cicXPath.ml
+++ b/helm/ocaml/cic_annotations/cicXPath.ml
@@ -56,8 +56,7 @@ let get_ids_to_targets annobj =
    in
     let rec add_target_term t =
      match t with
-        C.ARel (id,_,_)
-      | C.AVar (id,_)
+        C.ARel (id,_,_,_)
       | C.AMeta (id,_,_)
       | C.ASort (id,_)
       | C.AImplicit id ->
@@ -75,46 +74,52 @@ 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.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) ;
+         set_target idbody (C.ConstantBody annobj) ;
          List.iter (function (cid,_,context, t) as annconj ->
            set_target cid (C.Conjecture annconj) ;
           List.iter 
@@ -131,9 +136,9 @@ let get_ids_to_targets annobj =
       | 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 ;