X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FequalityTactics.ml;h=5d995c49bb2c379a46e2c42941414d1229f53189;hb=e2b6af273ccee4b15fb26a5d5353a11624bd8b3c;hp=0b61e9595778354639878ca264fc85b832eb8076;hpb=4dad47b93729b5108a7de190faeb25fcf16aba5d;p=helm.git

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 0b61e9595..5d995c49b 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -254,7 +254,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 +280,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:(