X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FequalityTactics.ml;h=8cb794ff6e17e918eefd4f0696276a41fc806822;hb=11b9b274291baa8c5462b2ce3e2a5f93a39c9d57;hp=4ff71c792a2af0f030b43102724c0f6d3d896d85;hpb=6bccccbe78dd8ca020038c0d7a901cd5b129fd03;p=helm.git

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 4ff71c792..8cb794ff6 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -56,11 +56,11 @@ let rewrite_tac ~term:equality ~status:(proof,goal) =
      let gty'' =
       ProofEngineReduction.replace_lifting
        ~equality:ProofEngineReduction.alpha_equivalence
-       ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
+       ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
      in
-      C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
+      C.Lambda
+       (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
     in
-prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
     let fresh_meta = ProofEngineHelpers.new_meta proof in
     let irl =
      ProofEngineHelpers.identity_relocation_list_for_metavariable context in
@@ -118,11 +118,11 @@ let rewrite_back_tac ~term:equality ~status:(proof,goal) =
      let gty'' =
       ProofEngineReduction.replace_lifting
        ~equality:ProofEngineReduction.alpha_equivalence
-       ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
+       ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
      in
-      C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
+      C.Lambda
+       (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
     in
-prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
     let fresh_meta = ProofEngineHelpers.new_meta proof in
     let irl =
      ProofEngineHelpers.identity_relocation_list_for_metavariable context in