From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 29 Jan 2003 17:09:47 +0000 (+0000)
Subject: ProofEngineHelpers.mk_fresh_name now used in place of "dummy_for_rewrite".
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6990ea89c3f7a4003b3afaec9989388d58f9a0b5;p=helm.git

ProofEngineHelpers.mk_fresh_name now used in place of "dummy_for_rewrite".
---

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 4ff71c792..36704b441 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -58,9 +58,9 @@ let rewrite_tac ~term:equality ~status:(proof,goal) =
        ~equality:ProofEngineReduction.alpha_equivalence
        ~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
@@ -120,9 +120,9 @@ let rewrite_back_tac ~term:equality ~status:(proof,goal) =
        ~equality:ProofEngineReduction.alpha_equivalence
        ~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