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

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

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 395768db96088a65abb4b63fed6bb5650d665095..04959e6962fdc2bd246db1282ae516682e5c837b 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -33,7 +33,7 @@ let assumption_tac ~status:((proof,goal) as status) =
   let module R = CicReduction in
   let module S = CicSubstitution 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 rec find n = function 
         hd::tl -> 
          (match hd with
@@ -66,7 +66,7 @@ let generalize_tac
   let module P = PrimitiveTactics in
   let module T = Tacticals 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 typ =
      match terms with
         [] -> assert false