X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FreductionTactics.ml;h=5a567b84aa75e6056814d845ea1a35e6d81a6120;hb=e9f24f9763283b44fcef456177f0390b51db7779;hp=55eacc234c3da15ffb057255dc73cf30391407f1;hpb=265cf771fbfe217b5f274b999fc3ad887683a09a;p=helm.git

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index 55eacc234..5a567b84a 100644
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -26,7 +26,7 @@
 (*
 let reduction_tac ~reduction ~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
   let new_ty = reduction context ty in
    let new_metasenv = 
     List.map
@@ -42,7 +42,7 @@ let reduction_tac ~reduction ~status:(proof,goal) =
 (* The default of term is the thesis of the goal to be prooved *)
 let reduction_tac ~also_in_hypotheses ~reduction ~terms ~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
   let terms =
    match terms with None -> [ty] | Some l -> l
   in
@@ -95,7 +95,7 @@ let whd_tac = reduction_tac ~reduction:CicReduction.whd ;;
 
 let fold_tac ~reduction ~also_in_hypotheses ~term ~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
   let term' = reduction context term in
    (* We don't know if [term] is a subterm of [ty] or a subterm of *)
    (* the type of one metavariable. So we replace it everywhere.   *)