Conjectures and Hypotheses inside every conjecture and in the sequents now

[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 76cb7f75ae9167690aa91575a2c6493e69b37382..eef9880bcfb6eef4aa6acd674a5a3418735a3078 100644 (file)
--- a/helm/ocaml/cic_annotations/cicXPath.ml
+++ b/helm/ocaml/cic_annotations/cicXPath.ml
@@ -116,13 +116,16 @@ 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 (_,context, t) -> 
+         List.iter (function (cid,_,context, t) as annconj ->
+           set_target cid (C.Conjecture annconj) ;
           List.iter 
-            (function 
-                Some (_,C.ADecl at) -> add_target_term at
-              | Some (_,C.ADef at) -> add_target_term at
-              | None -> ()
-            ) context; 
+            (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