Very experimental commit: the type of the source is now required in LetIns

[helm.git] / helm / software / components / tactics / variousTactics.ml

diff --git a/helm/software/components/tactics/variousTactics.ml b/helm/software/components/tactics/variousTactics.ml
index 3a3db7db43c4cf8cd1c0079b35ce6969ef89b24f..5563f206b057956509a4e973adfbabda1f907e66 100644 (file)
--- a/helm/software/components/tactics/variousTactics.ml
+++ b/helm/software/components/tactics/variousTactics.ml
@@ -46,15 +46,9 @@ let assumption_tac =
              (Some (_, C.Decl t)) when
                fst (R.are_convertible context (S.lift n t) ty 
                       CicUniv.empty_ugraph) -> n
-           | (Some (_, C.Def (_,Some ty'))) when
+           | (Some (_, C.Def (_,ty'))) when
                fst (R.are_convertible context (S.lift n ty') ty
                        CicUniv.empty_ugraph) -> n
-           | (Some (_, C.Def (t,None))) ->
-              let ty_t, u = (* TASSI: FIXME *)
-                CicTypeChecker.type_of_aux' metasenv context (S.lift n t) 
-                  CicUniv.empty_ugraph in
-              let b,_ = R.are_convertible context ty_t ty u in
-                if b then n else find (n+1) tl
            | _ -> find (n+1) tl
          )
       | [] -> raise (PET.Fail (lazy "Assumption: No such assumption"))