Defs in context may now have an optional type (when unknown).

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

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 390d97fb774b306baa0ea183612ea75ea1c961f7..395768db96088a65abb4b63fed6bb5650d665095 100644 (file)
--- 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