X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FequalityTactics.ml;h=82c339ae2b3d13381b6f1fee090eb1721f190fb9;hb=d97f69b313893900ca2d57544fcd200eb06ee286;hp=72a63571cef7221ae211360b5d44f58ba36a2f20;hpb=04858c4692eb584390fb53c7034ed7618431a9c0;p=helm.git

diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml
index 72a63571c..82c339ae2 100644
--- a/helm/software/components/tactics/equalityTactics.ml
+++ b/helm/software/components/tactics/equalityTactics.ml
@@ -70,15 +70,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
    match hyps_pat with
       [] -> None,true,(fun ~term _ -> P.exact_tac term),concl_pat,gty
     | [name,pat] ->
-      let rec find_hyp n =
-       function
-          [] -> assert false
-        | Some (Cic.Name s,Cic.Decl ty)::_ when name = s ->
-           Cic.Rel n, S.lift n ty
-        | Some (Cic.Name s,Cic.Def _)::_ when name = s -> assert false (*CSC: not implemented yet! But does this make any sense?*)
-        | _::tl -> find_hyp (n+1) tl
-      in
-       let arg,gty = find_hyp 1 context in
+       let arg,gty = ProofEngineHelpers.find_hyp name context in
        let dummy = "dummy" in
         Some arg,false,
          (fun ~term typ ->
@@ -104,7 +96,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
   in
   let ty_eq,ugraph = 
     CicTypeChecker.type_of_aux' metasenv context equality 
-      CicUniv.empty_ugraph in 
+      CicUniv.oblivion_ugraph in 
   let (ty_eq,metasenv',arguments,fresh_meta) =
    TermUtil.saturate_term
     (ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq 0 in  
@@ -241,7 +233,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
   in
   let context_len = List.length context in
   let subst,metasenv,u,_,selected_terms_with_context =
-   ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
+   ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph
     ~conjecture ~pattern in
   let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
   let with_what, metasenv, u = with_what context metasenv u in
@@ -251,7 +243,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
   let status = (uri,metasenv,_subst,pbo,pty, attrs),goal in
   let ty_of_with_what,u =
    CicTypeChecker.type_of_aux'
-    metasenv context with_what CicUniv.empty_ugraph in
+    metasenv context with_what CicUniv.oblivion_ugraph in
   let whats =
    match selected_terms_with_context with
       [] -> raise (ProofEngineTypes.Fail (lazy "Replace: no term selected"))
@@ -278,7 +270,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
              (lazy "Replace: one of the selected terms is not closed")) in
          let ty_of_t_in_context,u = (* TASSI: FIXME *)
           CicTypeChecker.type_of_aux' metasenv context t_in_context
-           CicUniv.empty_ugraph in
+           CicUniv.oblivion_ugraph in
          let b,u = CicReduction.are_convertible ~metasenv context
           ty_of_with_what ty_of_t_in_context u in
          if b then