split into two major parts:

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

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 390d97fb774b306baa0ea183612ea75ea1c961f7..64b9ff790618c6305938d685229ecbb73c6801be 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -33,13 +33,15 @@ let assumption_tac ~status:((proof,goal) as status) =
   let module R = CicReduction in
   let module S = CicSubstitution in
    let _,metasenv,_,_ = proof in
-    let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+    let _,context,ty = CicUtil.lookup_meta goal metasenv in
      let rec find n = function 
         hd::tl -> 
          (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
@@ -57,14 +59,14 @@ e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
 contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
 
 let generalize_tac
- ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name)
+ ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
  terms ~status:((proof,goal) as status)
 =
   let module C = Cic in
   let module P = PrimitiveTactics in
   let module T = Tacticals in
    let _,metasenv,_,_ = proof in
-   let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+   let _,context,ty = CicUtil.lookup_meta goal metasenv in
     let typ =
      match terms with
         [] -> assert false
@@ -81,7 +83,7 @@ let generalize_tac
       ~start:
         (P.cut_tac 
          (C.Prod(
-           (mk_fresh_name_callback context C.Anonymous typ), 
+           (mk_fresh_name_callback metasenv context C.Anonymous typ), 
            typ,
            (ProofEngineReduction.replace_lifting_csc 1
              ~equality:(==)