s/List.find.../CicUtil.lookup_meta/

[helm.git] / helm / ocaml / tactics / eliminationTactics.ml

diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml
index b6141094fc2c7cbd2cb8be8c2e2cf34131b1fe2f..cd401a2ec94cdaa66a0200c3bb516907b9ef3460 100644 (file)
--- a/helm/ocaml/tactics/eliminationTactics.ml
+++ b/helm/ocaml/tactics/eliminationTactics.ml
@@ -44,7 +44,7 @@ let induction_tac ~term ~status:((proof,goal) as status) =
   let module S = ProofEngineStructuralRules in
   let module U = UriManager in 
    let (_,metasenv,_,_) = proof in
-    let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+    let _,context,ty = CicUtil.lookup_meta goal metasenv in
      let termty = CicTypeChecker.type_of_aux' metasenv context term in (* per ora non serve *)
 
      T.then_ ~start:(T.repeat_tactic 
@@ -137,7 +137,7 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term ~status:((proof
   let module T = Tacticals in
   let module S = ProofEngineStructuralRules in
    let _,metasenv,_,_ = proof in
-    let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+    let _,context,ty = CicUtil.lookup_meta goal metasenv in
      let old_context_len = List.length context in
      let termty = CicTypeChecker.type_of_aux' metasenv context term in
 
@@ -178,7 +178,7 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term ~status:((proof
          warn ("nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim));
          if nr_of_hyp_still_to_elim <> 0 then
           let _,metasenv,_,_ = proof in
-           let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+           let _,context,_ = CicUtil.lookup_meta goal metasenv in
             let old_context_len = List.length context in
             let termty = CicTypeChecker.type_of_aux' metasenv context term' in
              warn ("elim_clear termty= " ^ CicPp.ppterm termty);
@@ -193,7 +193,7 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term ~status:((proof
                         (* clear the hyp that has just been eliminated *)
                         (fun ~status:((proof,goal) as status) -> 
                           let _,metasenv,_,_ = proof in
-                           let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+                           let _,context,_ = CicUtil.lookup_meta goal metasenv in
                             let new_context_len = List.length context in   
                              warn ("newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim));
                              let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim + (new_context_len - old_context_len) - 1 in