X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FvariousTactics.ml;h=5563f206b057956509a4e973adfbabda1f907e66;hb=cc23f034c9419186602d9250456241f2eba90d7c;hp=16a9c2267779cb27bb00866bdbf4751f70f0bb7a;hpb=61a2faa2694907757dd617175e0144705e79d65a;p=helm.git

diff --git a/helm/software/components/tactics/variousTactics.ml b/helm/software/components/tactics/variousTactics.ml
index 16a9c2267..5563f206b 100644
--- a/helm/software/components/tactics/variousTactics.ml
+++ b/helm/software/components/tactics/variousTactics.ml
@@ -38,7 +38,7 @@ let assumption_tac =
   let module R = CicReduction in
   let module S = CicSubstitution in
   let module PT = PrimitiveTactics in
-  let _,metasenv,_,_, _ = proof in
+  let _,metasenv,_subst,_,_, _ = proof in
   let _,context,ty = CicUtil.lookup_meta goal metasenv in
   let rec find n = function 
       hd::tl -> 
@@ -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"))
@@ -83,7 +77,7 @@ let generalize_tac
    let module C = Cic in
    let module P = PrimitiveTactics in
    let module T = Tacticals in
-    let uri,metasenv,pbo,pty, attrs = proof in
+    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
@@ -157,7 +151,7 @@ let generalize_tac
          else
           u1
       ) u terms_with_context) ;
-    let status = (uri,metasenv',pbo,pty, attrs),goal in
+    let status = (uri,metasenv',_subst,pbo,pty, attrs),goal in
     let proof,goals =
      PET.apply_tactic 
       (T.thens 
@@ -177,7 +171,7 @@ let generalize_tac
             T.id_tac])
         status
     in
-     let _,metasenv'',_,_, _ = proof in
+     let _,metasenv'',_subst,_,_, _ = proof in
       (* CSC: the following is just a bad approximation since a meta
          can be closed and then re-opened! *)
       (proof,