added fix for marangon

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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 0b61e9595778354639878ca264fc85b832eb8076..da7f599a9ec2b642291173c3d0c6c1d4a6fc5bf6 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -22,6 +22,8 @@
  * For details, see the HELM World-Wide-Web page,
  * http://cs.unibo.it/helm/.
  *)
+
+(* $Id$ *)
  
 let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equality =
  let _rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status
@@ -65,14 +67,7 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit
         | _::tl -> find_hyp (n+1) tl
       in
        let arg,gty = find_hyp 1 context in
-       let last_hyp_name_of_status (proof,goal) =
-        let curi, metasenv, pbo, pty = proof in
-        let metano,context,gty = CicUtil.lookup_meta goal metasenv in
-         match context with
-            (Some (Cic.Name s,_))::_ -> s
-          | _ -> assert false
-       in
-        let dummy = "dummy" in
+       let dummy = "dummy" in
         Some arg,false,
          (fun ~term typ ->
            Tacticals.seq
@@ -168,7 +163,7 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit
         metasenv', C.Meta (fresh_meta,irl), Cic.Rel (-1) (* dummy term, never used *)
     | Some arg ->
        let gty' = CicSubstitution.subst t1 abstr_gty in
-        metasenv,arg,gty'
+        metasenv',arg,gty'
   in
   let exact_proof = 
     C.Appl [eq_ind ; ty ; t2 ; pred ; arg ; t1 ;equality]
@@ -254,7 +249,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
           ty_of_with_what ty_of_t_in_context u in
          if b then
           let concl_pat_for_t = ProofEngineHelpers.pattern_of ~term:ty [t] in
-          let pattern_for_t = None,[],concl_pat_for_t in
+          let pattern_for_t = None,[],Some concl_pat_for_t in
            t_in_context,pattern_for_t
          else
           raise
@@ -280,7 +275,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
             ~continuations:[            
               T.then_
                 ~start:(
-                  rewrite_tac ~direction:`LeftToRight ~pattern (C.Rel 1))
+                  rewrite_tac ~direction:`LeftToRight ~pattern:lazy_pattern (C.Rel 1))
                  ~continuation:(
                    T.then_
                     ~start:(