X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FvariousTactics.ml;h=28dc4575d6f9e7ac56ac78ad3e5526883cb55725;hb=70182b25d7ff2961e1695b9f8b8a909ff07647be;hp=3a3db7db43c4cf8cd1c0079b35ce6969ef89b24f;hpb=c6cc2a7227d6750076f591a62d7b1896ebf1ebfa;p=helm.git

diff --git a/helm/software/components/tactics/variousTactics.ml b/helm/software/components/tactics/variousTactics.ml
index 3a3db7db4..28dc4575d 100644
--- a/helm/software/components/tactics/variousTactics.ml
+++ b/helm/software/components/tactics/variousTactics.ml
@@ -45,16 +45,10 @@ let assumption_tac =
         (match hd with
              (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
+		       CicUniv.oblivion_ugraph) -> n
+           | (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
+                       CicUniv.oblivion_ugraph) -> n
            | _ -> find (n+1) tl
          )
       | [] -> raise (PET.Fail (lazy "Assumption: No such assumption"))
@@ -86,7 +80,7 @@ let generalize_tac
     let uri,metasenv,_subst,pbo,pty, attrs = proof in
     let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
     let subst,metasenv,u,selected_hyps,terms_with_context =
-     ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
+     ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph
       ~conjecture ~pattern in
     let context = CicMetaSubst.apply_subst_context subst context in
     let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in