X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineStructuralRules.ml;h=7f4a89fb868bb0da871403047dc7dc4cd922d3a7;hb=d19f6472f195b5181fbda3746b6d632bc671eb57;hp=07ddf3a9ea4c77c430f3fe5c00d163e6abda76ee;hpb=265cf771fbfe217b5f274b999fc3ad887683a09a;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml
index 07ddf3a9e..7f4a89fb8 100644
--- a/helm/ocaml/tactics/proofEngineStructuralRules.ml
+++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml
@@ -33,7 +33,7 @@ let clearbody ~hyp ~status:(proof, goal) =
    | Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
    | Some (n_to_clear_body, C.Def (term,None)) as hyp_to_clear_body ->
       let curi,metasenv,pbo,pty = proof in
-       let metano,_,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+       let metano,_,_ = CicUtil.lookup_meta goal metasenv in
         let string_of_name =
          function
             C.Name n -> n
@@ -98,7 +98,7 @@ let clear ~hyp:hyp_to_clear ~status:(proof, goal) =
    | Some (n_to_clear, _) ->
       let curi,metasenv,pbo,pty = proof in
        let metano,context,ty =
-        List.find (function (m,_,_) -> m=goal) metasenv
+        CicUtil.lookup_meta goal metasenv
        in
         let string_of_name =
          function