From 6990ea89c3f7a4003b3afaec9989388d58f9a0b5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 29 Jan 2003 17:09:47 +0000 Subject: [PATCH] ProofEngineHelpers.mk_fresh_name now used in place of "dummy_for_rewrite". --- helm/ocaml/tactics/equalityTactics.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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 -- 2.39.2