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

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

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index c1297a0e555eb0cd6cb3bc47dcf76b87fb749096..518c6f86acc5daaa36c3724c2b404276972020dd 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -229,7 +229,7 @@ let apply_tac ~term ~status:(proof, goal) =
  let module R = CicReduction in
  let module C = Cic in
   let (_,metasenv,_,_) = proof in
-  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let newmeta = new_meta_of_proof ~proof in
    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
     match term with
@@ -318,7 +318,7 @@ let intros_tac
  let module C = Cic in
  let module R = CicReduction in
   let (_,metasenv,_,_) = proof in
-  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
    let newmeta = new_meta_of_proof ~proof in
     let (context',ty',bo') =
      lambda_abstract context newmeta ty mk_fresh_name_callback
@@ -334,7 +334,7 @@ let cut_tac
 =
  let module C = Cic in
   let curi,metasenv,pbo,pty = proof in
-  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
    let newmeta1 = new_meta_of_proof ~proof in
    let newmeta2 = newmeta1 + 1 in
    let fresh_name =
@@ -366,7 +366,7 @@ let letin_tac
 =
  let module C = Cic in
   let curi,metasenv,pbo,pty = proof in
-  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
    let _ = CicTypeChecker.type_of_aux' metasenv context term in
     let newmeta = new_meta_of_proof ~proof in
     let fresh_name =
@@ -389,7 +389,7 @@ let letin_tac
 let exact_tac ~term ~status:(proof, goal) =
  (* Assumption: the term bo must be closed in the current context *)
  let (_,metasenv,_,_) = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
  let module T = CicTypeChecker in
  let module R = CicReduction in
  if R.are_convertible context (T.type_of_aux' metasenv context term) ty then
@@ -410,7 +410,7 @@ let elim_tac ~term ~status:(proof, goal) =
  let module R = CicReduction in
  let module C = Cic in
   let (curi,metasenv,_,_) = proof in
-  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
    let termty = T.type_of_aux' metasenv context term in
    let uri,exp_named_subst,typeno,args =
     match termty with
@@ -450,7 +450,7 @@ let elim_tac ~term ~status:(proof, goal) =
         (* way.                                                         *)
         let meta_of_corpse =
          let (_,canonical_context,_) =
-          List.find (function (m,_,_) -> m=(lastmeta - 1)) newmetas
+           CicUtil.lookup_meta (lastmeta - 1) newmetas
          in
           let irl =
            CicMkImplicit.identity_relocation_list_for_metavariable
@@ -549,7 +549,7 @@ exception NotConvertible
 (*CSC: Is that evident? Is that right? Or should it be changed?              *)
 let change_tac ~what ~with_what ~status:(proof, goal) =
  let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   (* are_convertible works only on well-typed terms *)
   ignore (CicTypeChecker.type_of_aux' metasenv context with_what) ;
   if CicReduction.are_convertible context what with_what then