X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FvariousTactics.ml;h=395768db96088a65abb4b63fed6bb5650d665095;hb=265cf771fbfe217b5f274b999fc3ad887683a09a;hp=390d97fb774b306baa0ea183612ea75ea1c961f7;hpb=edf601b6b8eb5b28a5292d0660a3b54b5680e580;p=helm.git

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 390d97fb7..395768db9 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -39,7 +39,9 @@ let assumption_tac ~status:((proof,goal) as status) =
          (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