X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FvariousTactics.ml;h=04959e6962fdc2bd246db1282ae516682e5c837b;hb=f4b9cc6f689b52e0408ac3231ba2a480d71216fb;hp=390d97fb774b306baa0ea183612ea75ea1c961f7;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 390d97fb7..04959e696 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -33,13 +33,15 @@ 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
              (Some (_, C.Decl t)) when
                (R.are_convertible context (S.lift n t) ty) -> n
-           | (Some (_, C.Def t)) when
+           | (Some (_, C.Def (_,Some ty'))) when
+               (R.are_convertible context ty' ty) -> n
+           | (Some (_, C.Def (t,None))) when
                (R.are_convertible context
                 (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n 
            | _ -> find (n+1) tl
@@ -64,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