From da3c6e228c3c7ec75c8fd80e8fd7846327eb1b39 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 17 Nov 2005 18:19:39 +0000 Subject: [PATCH] Major code semplification and improvement: 1. the proof term generated used to have a (Hletin) ... Now it has a (H) ... 2. the code has been greatly simplified by renaming the old variable first and doing a letin later; I used to do the letin first and rename the new variable at the end --- helm/ocaml/tactics/equalityTactics.ml | 26 +++++++++----------------- 1 file changed, 9 insertions(+), 17 deletions(-) diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 2b2afae67..20dede31e 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -58,27 +58,19 @@ let rewrite_tac ~direction ~pattern equality = (Some (Cic.Name s,_))::_ -> s | _ -> assert false in + let dummy = "dummy" in Some arg,false, (fun ~term -> Tacticals.seq ~tactics: - [PT.letin_tac term; - PET.mk_tactic (fun status -> - PET.apply_tactic - (ProofEngineStructuralRules.clearbody - (last_hyp_name_of_status status)) status); - PET.mk_tactic (fun status -> - let hyp = last_hyp_name_of_status status in - PET.apply_tactic - (ReductionTactics.simpl_tac - ~pattern: - (None,[hyp,Cic.Implicit (Some `Hole)],Cic.Implicit None)) - status); - ProofEngineStructuralRules.clear name; - PET.mk_tactic (fun status -> - let hyp = last_hyp_name_of_status status in - PET.apply_tactic - (ProofEngineStructuralRules.rename hyp name) status) + [ProofEngineStructuralRules.rename name dummy; + PT.letin_tac + ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name name) term; + ProofEngineStructuralRules.clearbody name; + ReductionTactics.simpl_tac + ~pattern: + (None,[name,Cic.Implicit (Some `Hole)],Cic.Implicit None); + ProofEngineStructuralRules.clear dummy ]), pat,gty | _ -> assert false (*CSC: not implemented yet!*) -- 2.39.2